src/HOL/Tools/res_atp.ML
changeset 16515 7896ea4f3a87
parent 16478 d0a1f6231e2f
child 16520 7a9cda53bfa2
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Jun 21 11:08:31 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Jun 21 13:34:24 2005 +0200
     1.3 @@ -153,18 +153,15 @@
     1.4  (* should be modified to allow other provers to be called            *)
     1.5  (*********************************************************************)
     1.6  (* now passing in list of skolemized thms and list of sgterms to go with them *)
     1.7 -fun call_resolve_tac  (thms: Thm.thm list list)  sign (sg_terms:  Term.term list) (childin, childout,pid) n  = let
     1.8 +fun call_resolve_tac  (thms: Thm.thm list list)  sign (sg_terms:  Term.term list) (childin, childout,pid) n  = 
     1.9 + let
    1.10     val axfile = (File.platform_path axiom_file)
    1.11     val hypsfile = (File.platform_path hyps_file)
    1.12     val clasimpfile = (File.platform_path clasimp_file)
    1.13 -   val spass_home = getenv "SPASS_HOME"
    1.14 -   val spass = spass_home ^ "/SPASS"
    1.15 -   val _ = if File.exists (File.unpack_platform_path spass) then () 
    1.16 -	   else error ("Could not find the file " ^ spass)
    1.17       
    1.18     fun make_atp_list [] sign n = []
    1.19     |   make_atp_list ((sko_thm, sg_term)::xs) sign  n = 
    1.20 -   let 
    1.21 +     let 
    1.22  	val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 
    1.23  	val thmproofstr = proofstring ( skothmstr)
    1.24  	val no_returns =List.filter   not_newline ( thmproofstr)
    1.25 @@ -178,26 +175,32 @@
    1.26  	val _ = warning ("goalstring in make_atp_lists is: "^goalstring)
    1.27  
    1.28  	val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    1.29 -	val _ = (warning ("prob file in cal_res_tac is: "^probfile))                                                                           
    1.30 -in
    1.31 -     if !SpassComm.spass 
    1.32 -       then if !full_spass 
    1.33 -            then
    1.34 +	val _ = (warning ("prob file in cal_res_tac is: "^probfile))      
    1.35 +     in
    1.36 +       if !SpassComm.spass 
    1.37 +       then 
    1.38 +         let val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    1.39 +         in  (*We've checked that SPASS is there for ATP/spassshell to run.*)
    1.40 +           if !full_spass 
    1.41 +            then (*Allow SPASS to run in Auto mode, using all its inference rules*)
    1.42     		([("spass", thmstr, goalstring (*,spass_home*), 
    1.43 -	    	 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*),  
    1.44 +	    	 getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
    1.45  	     	"-DocProof%-TimeLimit=60", 
    1.46  	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    1.47 -  	    else	
    1.48 +  	    else (*Restrict SPASS to a small set of rules that we can parse*)
    1.49     		([("spass", thmstr, goalstring (*,spass_home*), 
    1.50  	     	getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*),  
    1.51  	     	"-Auto=0%-IORe%-IOFc%-RTaut%-RFSub%-RBSub%-DocProof%-TimeLimit=60", 
    1.52  	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    1.53 +	 end
    1.54       else
    1.55 -	   ([("vampire", thmstr, goalstring (*,spass_home*), 
    1.56 -	    	 "/homes/jm318/Vampire8/vkernel"(*( getenv "SPASS_HOME")^"/SPASS"*),  
    1.57 -	     	"-t 300%-m 100000", 
    1.58 -	     	clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    1.59 -end
    1.60 +       let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
    1.61 +       in  
    1.62 +	   ([("vampire", thmstr, goalstring, vampire, "-t 300%-m 100000", 
    1.63 +	      clasimpfile, axfile, hypsfile, probfile)] @ 
    1.64 +	    (make_atp_list xs sign (n+1)))
    1.65 +       end
    1.66 +     end
    1.67  
    1.68  val thms_goals = ListPair.zip( thms, sg_terms) 
    1.69  val atp_list = make_atp_list  thms_goals sign 1
    1.70 @@ -228,14 +231,14 @@
    1.71  
    1.72  
    1.73  fun get_sko_thms tfrees sign sg_terms (childin, childout,pid)  thm n sko_thms  =
    1.74 -                       if (equal n 0) then 
    1.75 -				(call_resolve_tac  (rev sko_thms) sign  sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm)
    1.76 -			else
    1.77 -                           
    1.78 -               		( SELECT_GOAL
    1.79 -  				(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    1.80 -  				 METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees;
    1.81 -                                                    get_sko_thms  tfrees sign sg_terms (childin, childout, pid) thm  (n -1) (negs::sko_thms);dummy_tac))]) n thm )
    1.82 +    if n=0 then 
    1.83 +	     (call_resolve_tac  (rev sko_thms) sign  sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm)
    1.84 +     else
    1.85 +	
    1.86 +     ( SELECT_GOAL
    1.87 +	     (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    1.88 +	      METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees;
    1.89 +				 get_sko_thms  tfrees sign sg_terms (childin, childout, pid) thm  (n -1) (negs::sko_thms);dummy_tac))]) n thm )
    1.90  
    1.91  
    1.92  
    1.93 @@ -246,21 +249,19 @@
    1.94  (**********************************************)
    1.95  
    1.96  fun isar_atp_goal' thm n tfree_lits  (childin, childout, pid) = 
    1.97 -                  
    1.98 -                           (let val  prems = prems_of thm 
    1.99 -                              (*val sg_term = get_nth k prems*)
   1.100 -                                val sign = sign_of_thm thm
   1.101 -                                val thmstring = string_of_thm thm
   1.102 -                            in   
   1.103 -                                 
   1.104 -                		(warning("in isar_atp_goal'"));
   1.105 -                                (warning("thmstring in isar_atp_goal': "^thmstring));
   1.106 - 				(* go and call callResProvers with this subgoal *)
   1.107 - 				(* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   1.108 - 				(* recursive call to pick up the remaining subgoals *)
   1.109 -                                (* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   1.110 -                                get_sko_thms tfree_lits sign  prems (childin, childout, pid) thm n []
   1.111 -                            end);
   1.112 +    let val  prems = prems_of thm 
   1.113 +      (*val sg_term = get_nth k prems*)
   1.114 +	val sign = sign_of_thm thm
   1.115 +	val thmstring = string_of_thm thm
   1.116 +    in   
   1.117 +	warning("in isar_atp_goal'");
   1.118 +	warning("thmstring in isar_atp_goal': "^thmstring);
   1.119 +	(* go and call callResProvers with this subgoal *)
   1.120 +	(* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   1.121 +	(* recursive call to pick up the remaining subgoals *)
   1.122 +	(* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   1.123 +	get_sko_thms tfree_lits sign  prems (childin, childout, pid) thm n []
   1.124 +    end ;
   1.125  
   1.126  (*fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) = 
   1.127                (if (!debug) then warning (string_of_thm thm)