src/HOL/Tools/res_atp.ML
author quigley
Mon Jul 11 16:42:42 2005 +0200 (2005-07-11)
changeset 16767 2d4433759b8d
parent 16741 7a6c17b826c0
child 16802 6eeee59dac4c
permissions -rw-r--r--
Fixed some problems with the signal handler.
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory
     2 
     3     ID: $Id$
     4 
     5     Copyright 2004 University of Cambridge
     6 
     7 ATPs with TPTP format input.
     8 *)
     9 
    10 (*Jia: changed: isar_atp now processes entire proof context.  fetch thms from delta simpset/claset*)
    11 (*Claire: changed: added actual watcher calls *)
    12 
    13 
    14 signature RES_ATP = 
    15 sig  
    16 val trace_res : bool ref
    17 val subgoals: Thm.thm list
    18 val traceflag : bool ref
    19 val axiom_file : Path.T
    20 val hyps_file : Path.T
    21 val isar_atp : ProofContext.context * Thm.thm -> unit
    22 val prob_file : Path.T;
    23 (*val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic*)
    24 (*val atp_tac : int -> Tactical.tactic*)
    25 val debug: bool ref
    26 val full_spass: bool ref
    27 (*val spass: bool ref*)
    28 val vampire: bool ref
    29 val custom_spass :string list  ref
    30 end;
    31 
    32 structure ResAtp : RES_ATP =
    33 
    34 struct
    35 
    36 val subgoals = [];
    37 
    38 val traceflag = ref true;
    39 (* used for debug *)
    40 val debug = ref false;
    41 
    42 fun debug_tac tac = (warning "testing";tac);
    43 (* default value is false *)
    44 
    45 val full_spass = ref false;
    46 
    47 (* use spass as default prover *)
    48 (*val spass = ref true;*)
    49 
    50 val custom_spass = ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub","-DocProof","-TimeLimit=60"];
    51 val vampire = ref false;
    52 
    53 val trace_res = ref false;
    54 
    55 val skolem_tac = skolemize_tac;
    56 
    57 val num_of_clauses = ref 0;
    58 val clause_arr = Array.array(3500, ("empty", 0));
    59 
    60 
    61 val atomize_tac =
    62     SUBGOAL
    63      (fn (prop,_) =>
    64 	 let val ts = Logic.strip_assums_hyp prop
    65 	 in EVERY1 
    66 		[METAHYPS
    67 		     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
    68 	  REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    69      end);
    70 
    71 (* temporarily use these files, which will be loaded by Vampire *)
    72 val file_id_num =ref 0;
    73 
    74 fun new_prob_file () =  (file_id_num := (!file_id_num) + 1;"prob"^(string_of_int (!file_id_num)));
    75 
    76 
    77 val axiom_file = File.tmp_path (Path.basic "axioms");
    78 val clasimp_file = File.tmp_path (Path.basic "clasimp");
    79 val hyps_file = File.tmp_path (Path.basic "hyps");
    80 val prob_file = File.tmp_path (Path.basic "prob");
    81 val dummy_tac = PRIMITIVE(fn thm => thm );
    82 
    83  
    84 (**** for Isabelle/ML interface  ****)
    85 
    86 fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ")
    87 
    88 fun proofstring x = let val exp = explode x 
    89                     in
    90                         List.filter (is_proof_char ) exp
    91                     end
    92 
    93 
    94 
    95 (*
    96 fun call_atp_tac thms n = (tptp_inputs thms ; dummy_tac);
    97 
    98 *)
    99 
   100 (**** For running in Isar ****)
   101 
   102 (* same function as that in res_axioms.ML *)
   103 fun repeat_RS thm1 thm2 =
   104     let val thm1' =  thm1 RS thm2 handle THM _ => thm1
   105     in
   106 	if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
   107     end;
   108 
   109 (* a special version of repeat_RS *)
   110 fun repeat_someI_ex thm = repeat_RS thm someI_ex;
   111 
   112 (*********************************************************************)
   113 (* convert clauses from "assume" to conjecture. write to file "hyps" *)
   114 (* hypotheses of the goal currently being proved                     *)
   115 (*********************************************************************)
   116 (*perhaps have 2 different versions of this, depending on whether or not SpassComm.spass is set *)
   117 fun isar_atp_h thms =
   118         
   119     let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
   120         val prems' = map repeat_someI_ex prems
   121         val prems'' = make_clauses prems'
   122         val prems''' = ResAxioms.rm_Eps [] prems''
   123         val clss = map ResClause.make_conjecture_clause prems'''
   124 	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
   125 	val tfree_lits = ResLib.flat_noDup tfree_litss
   126         (* tfree clause is different in tptp and dfg versions *)
   127 	val tfree_clss = map ResClause.tfree_clause tfree_lits 
   128         val hypsfile = File.platform_path hyps_file
   129 	val out = TextIO.openOut(hypsfile)
   130     in
   131 	((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits) 
   132     end;
   133 
   134 
   135 (*********************************************************************)
   136 (* write out a subgoal as tptp clauses to the file "probN"           *)
   137 (* where N is the number of this subgoal                             *)
   138 (*********************************************************************)
   139 
   140 fun tptp_inputs_tfrees thms n tfrees = 
   141     let val _ = (warning ("in tptp_inputs_tfrees 0"))
   142         val clss = map (ResClause.make_conjecture_clause_thm) thms
   143          val _ = (warning ("in tptp_inputs_tfrees 1"))
   144 	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
   145         val _ = (warning ("in tptp_inputs_tfrees 2"))
   146 	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
   147          val _ = (warning ("in tptp_inputs_tfrees 3"))
   148         val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
   149 	val out = TextIO.openOut(probfile)
   150     in
   151 	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
   152     end;
   153 
   154 
   155 (*********************************************************************)
   156 (* write out a subgoal as DFG clauses to the file "probN"           *)
   157 (* where N is the number of this subgoal                             *)
   158 (*********************************************************************)
   159 (*
   160 fun dfg_inputs_tfrees thms n tfrees = 
   161     let val _ = (warning ("in dfg_inputs_tfrees 0"))
   162         val clss = map (ResClause.make_conjecture_clause_thm) thms
   163          val _ = (warning ("in dfg_inputs_tfrees 1"))
   164 	val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
   165         val _ = (warning ("in dfg_inputs_tfrees 2"))
   166 	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
   167          val _ = (warning ("in dfg_inputs_tfrees 3"))
   168         val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
   169 	val out = TextIO.openOut(probfile)
   170     in
   171 	(ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
   172     end;*)
   173 
   174 (*********************************************************************)
   175 (* call SPASS with settings and problem file for the current subgoal *)
   176 (* should be modified to allow other provers to be called            *)
   177 (*********************************************************************)
   178 (* now passing in list of skolemized thms and list of sgterms to go with them *)
   179 fun call_resolve_tac  (thms: Thm.thm list list)  sign (sg_terms:  Term.term list) (childin, childout,pid) n  = 
   180  let
   181    val axfile = (File.platform_path axiom_file)
   182 
   183     val hypsfile = (File.platform_path hyps_file)
   184      val clasimpfile = (File.platform_path clasimp_file)
   185     val spass_home = getenv "SPASS_HOME"
   186 
   187 
   188    fun make_atp_list [] sign n = []
   189    |   make_atp_list ((sko_thm, sg_term)::xs) sign  n = 
   190      let 
   191 
   192 	val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
   193 	val thmproofstr = proofstring ( skothmstr)
   194 	val no_returns =List.filter   not_newline ( thmproofstr)
   195 	val thmstr = implode no_returns
   196 	val _ = warning ("thmstring in make_atp_lists is: "^thmstr)
   197 
   198 	val sgstr = Sign.string_of_term sign sg_term 
   199 	val goalproofstring = proofstring sgstr
   200 	val no_returns =List.filter not_newline ( goalproofstring)
   201 	val goalstring = implode no_returns
   202 	val _ = warning ("goalstring in make_atp_lists is: "^goalstring)
   203 
   204 	val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
   205 
   206 	val _ = (warning ("prob file in cal_res_tac is: "^probfile))      
   207      in
   208        if !SpassComm.spass 
   209        then 
   210          let val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
   211          in  (*We've checked that SPASS is there for ATP/spassshell to run.*)
   212            if !full_spass 
   213             then (*Allow SPASS to run in Auto mode, using all its inference rules*)
   214 
   215    		([("spass", thmstr, goalstring (*,spass_home*), 
   216 
   217 	    	 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*),  
   218 	     	"-DocProof%-TimeLimit=60%-SOS", 
   219 
   220 	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
   221   	    else (*Restrict SPASS to a small set of rules that we can parse*)
   222    		([("spass", thmstr, goalstring (*,spass_home*), 
   223 	     	getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*),  
   224 	     	("-" ^ space_implode "%-" (!custom_spass)), 
   225 	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
   226 	 end
   227      else
   228        let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
   229        in  
   230 	   ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000", 
   231 	      clasimpfile, axfile, hypsfile, probfile)] @ 
   232 	    (make_atp_list xs sign (n+1)))
   233        end
   234      end
   235 
   236 val thms_goals = ListPair.zip( thms, sg_terms) 
   237 val atp_list = make_atp_list  thms_goals sign 1
   238 in
   239 	Watcher.callResProvers(childout,atp_list);
   240         warning("Sent commands to watcher!");
   241   	dummy_tac
   242  end
   243 
   244 (**********************************************************)
   245 (* write out the current subgoal as a tptp file, probN,   *)
   246 (* then call dummy_tac - should be call_res_tac           *)
   247 (**********************************************************)
   248 
   249 
   250 fun get_sko_thms tfrees sign sg_terms (childin, childout,pid)  thm n sko_thms  =
   251     if n=0 then 
   252 	     (call_resolve_tac  (rev sko_thms) sign  sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm)
   253      else
   254 	
   255      ( SELECT_GOAL
   256 	     (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
   257 	      METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees;
   258 				 get_sko_thms  tfrees sign sg_terms (childin, childout, pid) thm  (n -1) (negs::sko_thms);dummy_tac))]) n thm )
   259 
   260 
   261 
   262 (**********************************************)
   263 (* recursively call atp_tac_g on all subgoals *)
   264 (* sg_term is the nth subgoal as a term - used*)
   265 (* in proof reconstruction                    *)
   266 (**********************************************)
   267 
   268 fun isar_atp_goal' thm n tfree_lits  (childin, childout, pid) = 
   269     let val  prems = prems_of thm 
   270       (*val sg_term = get_nth k prems*)
   271 	val sign = sign_of_thm thm
   272 	val thmstring = string_of_thm thm
   273     in   
   274 	warning("in isar_atp_goal'");
   275 	warning("thmstring in isar_atp_goal': "^thmstring);
   276 	(* go and call callResProvers with this subgoal *)
   277 	(* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   278 	(* recursive call to pick up the remaining subgoals *)
   279 	(* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   280 	get_sko_thms tfree_lits sign  prems (childin, childout, pid) thm n []
   281     end ;
   282 
   283 
   284 
   285 (**************************************************)
   286 (* convert clauses from "assume" to conjecture.   *)
   287 (* i.e. apply make_clauses and then get tptp for  *)
   288 (* any hypotheses in the goal produced by assume  *)
   289 (* statements;                                    *)
   290 (* write to file "hyps"                           *)
   291 (**************************************************)
   292 
   293 
   294 fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) = 
   295     let val tfree_lits = isar_atp_h thms 
   296     in
   297 	(warning("in isar_atp_aux"));
   298          isar_atp_goal' thm n_subgoals tfree_lits   (childin, childout, pid)
   299     end;
   300 
   301 (******************************************************************)
   302 (* called in Isar automatically                                   *)
   303 (* writes out the current clasimpset to a tptp file               *)
   304 (* passes all subgoals on to isar_atp_aux for further processing  *)
   305 (* turns off xsymbol at start of function, restoring it at end    *)
   306 (******************************************************************)
   307 (*FIX changed to clasimp_file *)
   308 fun isar_atp' (ctxt,thms, thm) =
   309  if null (prems_of thm) then () 
   310  else
   311     let 
   312 	val _= (print_mode := (Library.gen_rems (op =) 
   313 	                       (! print_mode, ["xsymbols", "symbols"])))
   314         val _= (warning ("in isar_atp'"))
   315         val prems = prems_of thm
   316         val sign = sign_of_thm thm
   317         val thms_string = Meson.concat_with_and (map string_of_thm thms) 
   318         val thmstring = string_of_thm thm
   319         val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   320         
   321 	(* set up variables for writing out the clasimps to a tptp file *)
   322 	val (clause_arr, num_of_clauses) =
   323 	    ResClasimp.write_out_clasimp (File.platform_path clasimp_file) 
   324 	                                 (ProofContext.theory_of ctxt)
   325 	                                 (hd prems) (*FIXME: hack!! need to do all prems*)
   326         val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file) 
   327         val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses)
   328         val pidstring = string_of_int(Word.toInt
   329                            (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
   330     in
   331        warning ("initial thms: "^thms_string); 
   332        warning ("initial thm: "^thmstring);
   333        warning ("subgoals: "^prems_string);
   334        warning ("pid: "^ pidstring); 
   335        isar_atp_aux thms thm (length prems) (childin, childout, pid);
   336        warning("turning xsymbol back on!");
   337        print_mode := (["xsymbols", "symbols"] @ ! print_mode)
   338     end;
   339 
   340 
   341 
   342 
   343 local
   344 
   345 fun get_thms_cs claset =
   346     let val clsset = rep_cs claset
   347 	val safeEs = #safeEs clsset
   348 	val safeIs = #safeIs clsset
   349 	val hazEs = #hazEs clsset
   350 	val hazIs = #hazIs clsset
   351     in
   352 	safeEs @ safeIs @ hazEs @ hazIs
   353     end;
   354 
   355 
   356 
   357 fun append_name name [] _ = []
   358   | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
   359 
   360 fun append_names (name::names) (thms::thmss) =
   361     let val thms' = append_name name thms 0
   362     in
   363 	thms'::(append_names names thmss)
   364     end;
   365 
   366 
   367 fun get_thms_ss [] = []
   368   | get_thms_ss thms =
   369     let val names = map Thm.name_of_thm thms 
   370         val thms' = map (mksimps mksimps_pairs) thms
   371         val thms'' = append_names names thms'
   372     in
   373 	ResLib.flat_noDup thms''
   374     end;
   375 
   376 
   377 
   378 
   379 in
   380 
   381 
   382 (* convert locally declared rules to axiom clauses *)
   383 (* write axiom clauses to ax_file *)
   384 (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
   385 (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
   386 (*claset file and prob file*)
   387 (* FIX*)
   388 (*fun isar_local_thms (delta_cs, delta_ss_thms) =
   389     let val thms_cs = get_thms_cs delta_cs
   390 	val thms_ss = get_thms_ss delta_ss_thms
   391 	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
   392 	val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
   393 	val ax_file = File.platform_path axiom_file
   394 	val out = TextIO.openOut ax_file
   395     in
   396 	(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
   397     end;
   398 *)
   399 
   400 
   401 
   402 
   403 (* called in Isar automatically *)
   404 
   405 fun isar_atp (ctxt,thm) =
   406     let val prems = ProofContext.prems_of ctxt
   407         val d_cs = Classical.get_delta_claset ctxt 
   408         val d_ss_thms = Simplifier.get_delta_simpset ctxt
   409         val thmstring = string_of_thm thm
   410         val sg_prems = prems_of thm
   411         val sign = sign_of_thm thm
   412         val prem_no = length sg_prems
   413         val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) 
   414     in
   415           (warning ("initial thm in isar_atp: "^thmstring));
   416           (warning ("subgoals in isar_atp: "^prems_string));
   417     	  (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
   418           (*isar_local_thms (d_cs,d_ss_thms);*)
   419            isar_atp' (ctxt,prems, thm)
   420     end;
   421 
   422 end
   423 
   424 
   425 
   426 
   427 end;
   428 
   429 Proof.atp_hook := ResAtp.isar_atp;