src/HOL/Tools/res_atp.ML
changeset 17306 5cde710a8a23
parent 17305 6cef3aedd661
child 17317 3f12de2e2e6e
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Sep 07 09:54:31 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Sep 07 18:14:26 2005 +0200
     1.3 @@ -8,9 +8,7 @@
     1.4  signature RES_ATP =
     1.5  sig
     1.6    val axiom_file : Path.T
     1.7 -  val full_spass: bool ref
     1.8 -  val spass: bool ref
     1.9 -  val vampire: bool ref
    1.10 +  val prover: string ref
    1.11    val custom_spass: string list ref
    1.12    val hook_count: int ref
    1.13  end;
    1.14 @@ -24,9 +22,7 @@
    1.15  
    1.16  fun debug_tac tac = (debug "testing"; tac);
    1.17  
    1.18 -val vampire = ref false;   (* use Vampire as default prover? *)
    1.19 -val spass = ref true;      (* use spass as default prover *)
    1.20 -val full_spass = ref true;  (*specifies Auto mode: SPASS can use all inference rules*)
    1.21 +val prover = ref "spass";   (* use spass as default prover *)
    1.22  val custom_spass =   (*specialized options for SPASS*)
    1.23        ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
    1.24             "-DocProof","-TimeLimit=60"];
    1.25 @@ -130,8 +126,7 @@
    1.26  
    1.27  
    1.28  (*********************************************************************)
    1.29 -(* call SPASS with settings and problem file for the current subgoal *)
    1.30 -(* should be modified to allow other provers to be called            *)
    1.31 +(* call prover with settings and problem file for the current subgoal *)
    1.32  (*********************************************************************)
    1.33  (* now passing in list of skolemized thms and list of sgterms to go with them *)
    1.34  fun call_resolve_tac  (thms: thm list list)  sign (sg_terms:  term list) (childin, childout,pid) n  =
    1.35 @@ -152,12 +147,14 @@
    1.36              val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
    1.37              val _ = debug ("prob file in call_resolve_tac is " ^ probfile)
    1.38            in
    1.39 -            if !spass
    1.40 +            if !prover = "spass"
    1.41              then
    1.42 -              let val optionline = (*Custom SPASS options, or default?*)
    1.43 -		      if !full_spass (*Auto mode: all SPASS inference rules*)
    1.44 -                      then "-DocProof%-TimeLimit=60%-SOS"
    1.45 -                      else "-" ^ space_implode "%-" (!custom_spass)
    1.46 +              let val optionline = 
    1.47 +		      if !SpassComm.reconstruct 
    1.48 +		          (*Proof reconstruction works for only a limited set of 
    1.49 +		            inference rules*)
    1.50 +                      then "-" ^ space_implode "%-" (!custom_spass)
    1.51 +                      else "-DocProof%-TimeLimit=60%-SOS" (*Auto mode*)
    1.52                    val _ = debug ("SPASS option string is " ^ optionline)
    1.53                    val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    1.54                      (*We've checked that SPASS is there for ATP/spassshell to run.*)
    1.55 @@ -167,7 +164,7 @@
    1.56                       optionline, axfile, hypsfile, probfile)] @ 
    1.57                    (make_atp_list xs sign (n+1)))
    1.58                end
    1.59 -            else if !vampire 
    1.60 +            else if !prover = "vampire"
    1.61  	    then 
    1.62                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
    1.63                in
    1.64 @@ -175,14 +172,16 @@
    1.65                     axfile, hypsfile, probfile)] @
    1.66                   (make_atp_list xs sign (n+1)))
    1.67                end
    1.68 -      	     else
    1.69 -             let val Eprover = ResLib.helper_path "E_HOME" "eproof"
    1.70 -              in
    1.71 -                ([("E", thmstr, goalstring, Eprover, "--tptp-in -l5",
    1.72 -                   axfile, hypsfile, probfile)] @
    1.73 -                 (make_atp_list xs sign (n+1)))
    1.74 -              end
    1.75 -
    1.76 +      	     else if !prover = "E"
    1.77 +      	     then
    1.78 +	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
    1.79 +	       in
    1.80 +		  ([("E", thmstr, goalstring, Eprover, 
    1.81 +		     "--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60",
    1.82 +		     axfile, hypsfile, probfile)] @
    1.83 +		   (make_atp_list xs sign (n+1)))
    1.84 +	       end
    1.85 +	     else error ("Invalid prover name: " ^ !prover)
    1.86            end
    1.87  
    1.88      val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1
    1.89 @@ -205,15 +204,15 @@
    1.90          all_tac thm)
    1.91       else
    1.92  	
    1.93 -     ( SELECT_GOAL
    1.94 +      (SELECT_GOAL
    1.95          (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
    1.96            METAHYPS(fn negs => 
    1.97 -            (if !spass 
    1.98 +            (if !prover = "spass" 
    1.99               then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
   1.100               else tptp_inputs_tfrees (make_clauses negs) n tfrees axclauses;
   1.101               get_sko_thms tfrees sign sg_terms (childin, childout, pid) 
   1.102 -                          thm  (n -1) (negs::sko_thms) axclauses; 
   1.103 -             all_tac))]) n thm )
   1.104 +                          thm (n-1) (negs::sko_thms) axclauses; 
   1.105 +             all_tac))]) n thm)
   1.106  
   1.107  
   1.108  
   1.109 @@ -223,36 +222,20 @@
   1.110  (* in proof reconstruction                    *)
   1.111  (**********************************************)
   1.112  
   1.113 -fun isar_atp_goal' thm n tfree_lits (childin, childout, pid)  axclauses =
   1.114 -  let
   1.115 -    val prems = Thm.prems_of thm
   1.116 -    (*val sg_term = get_nth k prems*)
   1.117 -    val sign = sign_of_thm thm
   1.118 -    val thmstring = string_of_thm thm
   1.119 +fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) axclauses =
   1.120 +  let val tfree_lits = isar_atp_h thms
   1.121 +      val prems = Thm.prems_of thm
   1.122 +      val sign = sign_of_thm thm
   1.123 +      val thmstring = string_of_thm thm
   1.124    in
   1.125 -    debug("in isar_atp_goal'");
   1.126 +    debug ("in isar_atp_aux");
   1.127      debug("thmstring in isar_atp_goal': " ^ thmstring);
   1.128      (* go and call callResProvers with this subgoal *)
   1.129      (* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
   1.130      (* recursive call to pick up the remaining subgoals *)
   1.131      (* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
   1.132 -    get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n []  axclauses
   1.133 -  end;
   1.134 -
   1.135 -
   1.136 -(**************************************************)
   1.137 -(* convert clauses from "assume" to conjecture.   *)
   1.138 -(* i.e. apply make_clauses and then get tptp for  *)
   1.139 -(* any hypotheses in the goal produced by assume  *)
   1.140 -(* statements;                                    *)
   1.141 -(* write to file "hyps"                           *)
   1.142 -(**************************************************)
   1.143 -
   1.144 -fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) axclauses =
   1.145 -  let val tfree_lits = isar_atp_h thms
   1.146 -  in
   1.147 -    debug ("in isar_atp_aux");
   1.148 -    isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid)  axclauses
   1.149 +    get_sko_thms tfree_lits sign prems (childin, childout, pid) 
   1.150 +                 thm n_subgoals []  axclauses
   1.151    end;
   1.152  
   1.153  (******************************************************************)
   1.154 @@ -270,7 +253,6 @@
   1.155        val thy = ProofContext.theory_of ctxt
   1.156        val prems = Thm.prems_of thm
   1.157        val thms_string = Meson.concat_with_and (map string_of_thm thms)
   1.158 -      val thm_string = string_of_thm thm
   1.159        val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
   1.160  
   1.161        (*set up variables for writing out the clasimps to a tptp file*)
   1.162 @@ -282,7 +264,6 @@
   1.163          string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
   1.164      in
   1.165        debug ("initial thms: " ^ thms_string);
   1.166 -      debug ("initial thm: " ^ thm_string);
   1.167        debug ("subgoals: " ^ prems_string);
   1.168        debug ("pid: "^ pid_string);
   1.169        isar_atp_aux thms thm (length prems) (childin, childout, pid) axclauses;