src/HOL/Tools/res_atp.ML
author paulson
Fri Sep 09 17:47:37 2005 +0200 (2005-09-09)
changeset 17317 3f12de2e2e6e
parent 17306 5cde710a8a23
child 17404 d16c3a62c396
permissions -rw-r--r--
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
     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 axiom_file : Path.T
    11   val prover: string ref
    12   val custom_spass: string list ref
    13   val hook_count: int ref
    14 end;
    15 
    16 structure ResAtp: RES_ATP =
    17 struct
    18 
    19 
    20 val call_atp = ref false;
    21 val hook_count = ref 0;
    22 
    23 fun debug_tac tac = (debug "testing"; tac);
    24 
    25 val prover = ref "spass";   (* use spass as default prover *)
    26 val custom_spass =   (*specialized options for SPASS*)
    27       ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
    28            "-DocProof","-TimeLimit=60"];
    29 
    30 val axiom_file = File.tmp_path (Path.basic "axioms");
    31 val hyps_file = File.tmp_path (Path.basic "hyps");
    32 val prob_file = File.tmp_path (Path.basic "prob");
    33 
    34 
    35 (**** for Isabelle/ML interface  ****)
    36 
    37 (*Remove unwanted characters such as ? and newline from the textural 
    38   representation of a theorem (surely they don't need to be produced in 
    39   the first place?) *)
    40 
    41 fun is_proof_char ch = (#" " <= ch andalso ch <= #"~" andalso ch <> #"?");
    42 
    43 val proofstring =
    44     String.translate (fn c => if is_proof_char c then str c else "");
    45 
    46 
    47 (**** For running in Isar ****)
    48 
    49 (* same function as that in res_axioms.ML *)
    50 fun repeat_RS thm1 thm2 =
    51     let val thm1' =  thm1 RS thm2 handle THM _ => thm1
    52     in
    53         if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
    54     end;
    55 
    56 (* a special version of repeat_RS *)
    57 fun repeat_someI_ex thm = repeat_RS thm someI_ex;
    58 
    59 
    60 (*********************************************************************)
    61 (* convert clauses from "assume" to conjecture. write to file "hyps" *)
    62 (* hypotheses of the goal currently being proved                     *)
    63 (*********************************************************************)
    64 (*perhaps have 2 different versions of this, depending on whether or not spass is set *)
    65 fun isar_atp_h thms =
    66     let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
    67         val prems' = map repeat_someI_ex prems
    68         val prems'' = make_clauses prems'
    69         val prems''' = ResAxioms.rm_Eps [] prems''
    70         val clss = map ResClause.make_conjecture_clause prems'''
    71 	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
    72 	val tfree_lits = ResLib.flat_noDup tfree_litss
    73         (* tfree clause is different in tptp and dfg versions *)
    74 	val tfree_clss = map ResClause.tfree_clause tfree_lits 
    75         val hypsfile = File.platform_path hyps_file
    76         val out = TextIO.openOut(hypsfile)
    77     in
    78         ResLib.writeln_strs out (tfree_clss @ tptp_clss);
    79         TextIO.closeOut out; debug hypsfile;
    80         tfree_lits
    81     end;
    82 
    83 
    84 (*********************************************************************)
    85 (* write out a subgoal as tptp clauses to the file "probN"           *)
    86 (* where N is the number of this subgoal                             *)
    87 (*********************************************************************)
    88 
    89 fun tptp_inputs_tfrees thms n tfrees axclauses =
    90     let
    91       val _ = debug ("in tptp_inputs_tfrees 0")
    92       val clss = map (ResClause.make_conjecture_clause_thm) thms
    93       val _ = debug ("in tptp_inputs_tfrees 1")
    94       val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    95       val _ = debug ("in tptp_inputs_tfrees 2")
    96       val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees)
    97       val _ = debug ("in tptp_inputs_tfrees 3")
    98       val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
    99       val out = TextIO.openOut(probfile)
   100     in
   101       ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
   102       ResLib.writeln_strs out (tfree_clss @ tptp_clss);
   103       TextIO.closeOut out;
   104       debug probfile
   105     end;
   106 
   107 
   108 (*********************************************************************)
   109 (* write out a subgoal as DFG clauses to the file "probN"           *)
   110 (* where N is the number of this subgoal                             *)
   111 (*********************************************************************)
   112 
   113 fun dfg_inputs_tfrees thms n tfrees axclauses = 
   114     let val clss = map (ResClause.make_conjecture_clause_thm) thms
   115         val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
   116         val _ = debug ("about to write out dfg prob file " ^ probfile)
   117        	(*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
   118         val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *)   
   119         val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
   120                         axclauses [] [] [] tfrees   
   121 	val out = TextIO.openOut(probfile)
   122     in
   123 	(ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile )
   124 (* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *)
   125     end;
   126 
   127 
   128 (*********************************************************************)
   129 (* call prover with settings and problem file for the current subgoal *)
   130 (*********************************************************************)
   131 (* now passing in list of skolemized thms and list of sgterms to go with them *)
   132 fun call_resolve_tac  (thms: thm list list)  sign (sg_terms:  term list) (childin, childout,pid) n  =
   133   let
   134     val axfile = (File.platform_path axiom_file)
   135 
   136     val hypsfile = (File.platform_path hyps_file)
   137 
   138     fun make_atp_list [] sign n = []
   139       | make_atp_list ((sko_thm, sg_term)::xs) sign n =
   140           let
   141             val thmstr = proofstring (Meson.concat_with_and (map string_of_thm sko_thm))
   142             val _ = debug ("thmstring in make_atp_lists is " ^ thmstr)
   143 
   144             val goalstring = proofstring (Sign.string_of_term sign sg_term)
   145             val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
   146 
   147             val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
   148             val _ = debug ("prob file in call_resolve_tac is " ^ probfile)
   149           in
   150             (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
   151               versions of Unix.execute treat them differently!*)
   152             if !prover = "spass"
   153             then
   154               let val optionline = 
   155 		      if !SpassComm.reconstruct 
   156 		          (*Proof reconstruction works for only a limited set of 
   157 		            inference rules*)
   158                       then "-" ^ space_implode "%-" (!custom_spass)
   159                       else "-DocProof%-TimeLimit=60%-SOS%-FullRed=0" (*Auto mode*)
   160                   val _ = debug ("SPASS option string is " ^ optionline)
   161                   val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
   162                     (*We've checked that SPASS is there for ATP/spassshell to run.*)
   163               in 
   164                   ([("spass", thmstr, goalstring,
   165                      getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
   166                      optionline, axfile, hypsfile, probfile)] @ 
   167                   (make_atp_list xs sign (n+1)))
   168               end
   169             else if !prover = "vampire"
   170 	    then 
   171               let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
   172               in
   173                 ([("vampire", thmstr, goalstring, vampire, "-t60%-m100000",
   174                    axfile, hypsfile, probfile)] @
   175                  (make_atp_list xs sign (n+1)))
   176               end
   177       	     else if !prover = "E"
   178       	     then
   179 	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
   180 	       in
   181 		  ([("E", thmstr, goalstring, Eprover, 
   182 		     "--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60",
   183 		     axfile, hypsfile, probfile)] @
   184 		   (make_atp_list xs sign (n+1)))
   185 	       end
   186 	     else error ("Invalid prover name: " ^ !prover)
   187           end
   188 
   189     val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1
   190   in
   191     Watcher.callResProvers(childout,atp_list);
   192     debug "Sent commands to watcher!";
   193     all_tac
   194   end
   195 
   196 (**********************************************************)
   197 (* write out the current subgoal as a tptp file, probN,   *)
   198 (* then call all_tac - should be call_res_tac           *)
   199 (**********************************************************)
   200 
   201 
   202 fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms axclauses =
   203     if n=0 then 
   204        (call_resolve_tac  (rev sko_thms)
   205         sign  sg_terms (childin, childout, pid) (List.length sg_terms);
   206         all_tac thm)
   207      else
   208 	
   209       (SELECT_GOAL
   210         (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
   211           METAHYPS(fn negs => 
   212             (if !prover = "spass" 
   213              then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
   214              else tptp_inputs_tfrees (make_clauses negs) n tfrees axclauses;
   215              get_sko_thms tfrees sign sg_terms (childin, childout, pid) 
   216                           thm (n-1) (negs::sko_thms) axclauses; 
   217              all_tac))]) n thm)
   218 
   219 
   220 
   221 (**********************************************)
   222 (* recursively call atp_tac_g on all subgoals *)
   223 (* sg_term is the nth subgoal as a term - used*)
   224 (* in proof reconstruction                    *)
   225 (**********************************************)
   226 
   227 fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) axclauses =
   228   let val tfree_lits = isar_atp_h thms
   229       val prems = Thm.prems_of thm
   230       val sign = sign_of_thm thm
   231       val thmstring = string_of_thm thm
   232   in
   233     debug ("in isar_atp_aux");
   234     debug("thmstring in isar_atp_goal': " ^ thmstring);
   235     (* go and call callResProvers with this subgoal *)
   236     (* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   237     (* recursive call to pick up the remaining subgoals *)
   238     (* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   239     get_sko_thms tfree_lits sign prems (childin, childout, pid) 
   240                  thm n_subgoals []  axclauses
   241   end;
   242 
   243 (******************************************************************)
   244 (* called in Isar automatically                                   *)
   245 (* writes out the current clasimpset to a tptp file               *)
   246 (* passes all subgoals on to isar_atp_aux for further processing  *)
   247 (* turns off xsymbol at start of function, restoring it at end    *)
   248 (******************************************************************)
   249 (*FIX changed to clasimp_file *)
   250 val isar_atp' = setmp print_mode [] (fn (ctxt, thms, thm) =>
   251   if Thm.no_prems thm then ()
   252   else
   253     let
   254       val _= debug ("in isar_atp'")
   255       val thy = ProofContext.theory_of ctxt
   256       val prems = Thm.prems_of thm
   257       val thms_string = Meson.concat_with_and (map string_of_thm thms)
   258       val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
   259 
   260       (*set up variables for writing out the clasimps to a tptp file*)
   261       val (clause_arr, num_of_clauses, axclauses) =
   262         ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
   263       val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^ " clauses")
   264       val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr, num_of_clauses)
   265       val pid_string =
   266         string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
   267     in
   268       debug ("initial thms: " ^ thms_string);
   269       debug ("subgoals: " ^ prems_string);
   270       debug ("pid: "^ pid_string);
   271       isar_atp_aux thms thm (length prems) (childin, childout, pid) axclauses;
   272       ()
   273     end);
   274 
   275 
   276 fun get_thms_cs claset =
   277   let val {safeEs, safeIs, hazEs, hazIs, ...} = rep_cs claset
   278   in safeEs @ safeIs @ hazEs @ hazIs end;
   279 
   280 fun append_name name [] _ = []
   281   | append_name name (thm :: thms) k =
   282       Thm.name_thm ((name ^ "_" ^ string_of_int k), thm) :: append_name name thms (k + 1);
   283 
   284 fun append_names (name :: names) (thms :: thmss) =
   285   append_name name thms 0 :: append_names names thmss;
   286 
   287 fun get_thms_ss [] = []
   288   | get_thms_ss thms =
   289       let
   290         val names = map Thm.name_of_thm thms
   291         val thms' = map (mksimps mksimps_pairs) thms
   292         val thms'' = append_names names thms'
   293       in
   294         ResLib.flat_noDup thms''
   295       end;
   296 
   297 
   298 (* convert locally declared rules to axiom clauses *)
   299 
   300 fun subtract_simpset thy ctxt =
   301   let
   302     val rules1 = #rules (#1 (rep_ss (simpset_of thy)));
   303     val rules2 = #rules (#1 (rep_ss (local_simpset_of ctxt)));
   304   in map #thm (Net.subtract MetaSimplifier.eq_rrule rules1 rules2) end;
   305 
   306 fun subtract_claset thy ctxt =
   307   let
   308     val (netI1, netE1) = #xtra_netpair (rep_cs (claset_of thy));
   309     val (netI2, netE2) = #xtra_netpair (rep_cs (local_claset_of ctxt));
   310     val subtract = map (#2 o #2) oo Net.subtract Tactic.eq_kbrl;
   311   in subtract netI1 netI2 @ subtract netE1 netE2 end;
   312 
   313 
   314 
   315 (** the Isar toplevel hook **)
   316 
   317 val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   318   let
   319     val proof = Toplevel.proof_of state
   320     val (ctxt, (_, goal)) = Proof.get_goal proof
   321         handle Proof.STATE _ => error "No goal present";
   322 
   323     val thy = ProofContext.theory_of ctxt;
   324 
   325     (* FIXME presently unused *)
   326     val ss_thms = subtract_simpset thy ctxt;
   327     val cs_thms = subtract_claset thy ctxt;
   328   in
   329     debug ("initial thm in isar_atp: " ^ 
   330            Pretty.string_of (ProofContext.pretty_thm ctxt goal));
   331     debug ("subgoals in isar_atp: " ^ 
   332            Pretty.string_of (ProofContext.pretty_term ctxt
   333              (Logic.mk_conjunction_list (Thm.prems_of goal))));
   334     debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
   335     hook_count := !hook_count +1;
   336     debug ("in hook for time: " ^(string_of_int (!hook_count)) );
   337     ResClause.init thy;
   338     isar_atp' (ctxt, ProofContext.prems_of ctxt, goal)
   339   end);
   340 
   341 val call_atpP =
   342   OuterSyntax.improper_command 
   343     "ProofGeneral.call_atp" 
   344     "call automatic theorem provers" 
   345     OuterKeyword.diag
   346     (Scan.succeed (Toplevel.no_timing o invoke_atp));
   347 
   348 val _ = OuterSyntax.add_parsers [call_atpP];
   349 
   350 end;