src/HOL/Tools/res_atp.ML
changeset 17305 6cef3aedd661
parent 17235 8e55ad29b690
child 17306 5cde710a8a23
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Sep 07 09:53:50 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Sep 07 09:54:31 2005 +0200
     1.3 @@ -8,14 +8,11 @@
     1.4  signature RES_ATP =
     1.5  sig
     1.6    val axiom_file : Path.T
     1.7 -(*val atp_ax_tac : thm list -> int -> Tactical.tactic*)
     1.8 -(*val atp_tac : int -> Tactical.tactic*)
     1.9    val full_spass: bool ref
    1.10 -(*val spass: bool ref*)
    1.11 +  val spass: bool ref
    1.12    val vampire: bool ref
    1.13    val custom_spass: string list ref
    1.14    val hook_count: int ref
    1.15 -(*  val invoke_atp: Toplevel.transition -> Toplevel.transition*)
    1.16  end;
    1.17  
    1.18  structure ResAtp: RES_ATP =
    1.19 @@ -27,32 +24,14 @@
    1.20  
    1.21  fun debug_tac tac = (debug "testing"; tac);
    1.22  
    1.23 -val full_spass = ref false;
    1.24 -
    1.25 -(* use spass as default prover *)
    1.26 -(*val spass = ref true;*)
    1.27 -
    1.28 -val custom_spass = ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub","-DocProof","-TimeLimit=60"];
    1.29 -val vampire = ref false;
    1.30 -
    1.31 -val skolem_tac = skolemize_tac;
    1.32 -
    1.33 -val num_of_clauses = ref 0;
    1.34 -val clause_arr = Array.array (3500, ("empty", 0));
    1.35 -
    1.36 -
    1.37 -val atomize_tac =
    1.38 -    SUBGOAL
    1.39 -     (fn (prop,_) =>
    1.40 -         let val ts = Logic.strip_assums_hyp prop
    1.41 -         in EVERY1
    1.42 -                [METAHYPS
    1.43 -                     (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
    1.44 -          REPEAT_DETERM_N (length ts) o (etac thin_rl)]
    1.45 -     end);
    1.46 +val vampire = ref false;   (* use Vampire as default prover? *)
    1.47 +val spass = ref true;      (* use spass as default prover *)
    1.48 +val full_spass = ref true;  (*specifies Auto mode: SPASS can use all inference rules*)
    1.49 +val custom_spass =   (*specialized options for SPASS*)
    1.50 +      ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
    1.51 +           "-DocProof","-TimeLimit=60"];
    1.52  
    1.53  val axiom_file = File.tmp_path (Path.basic "axioms");
    1.54 -val clasimp_file = File.tmp_path (Path.basic "clasimp");
    1.55  val hyps_file = File.tmp_path (Path.basic "hyps");
    1.56  val prob_file = File.tmp_path (Path.basic "prob");
    1.57  
    1.58 @@ -82,12 +61,11 @@
    1.59  fun repeat_someI_ex thm = repeat_RS thm someI_ex;
    1.60  
    1.61  
    1.62 -(*FIXME: is function isar_atp_h used? If not, delete!*)
    1.63  (*********************************************************************)
    1.64  (* convert clauses from "assume" to conjecture. write to file "hyps" *)
    1.65  (* hypotheses of the goal currently being proved                     *)
    1.66  (*********************************************************************)
    1.67 -(*perhaps have 2 different versions of this, depending on whether or not SpassComm.spass is set *)
    1.68 +(*perhaps have 2 different versions of this, depending on whether or not spass is set *)
    1.69  fun isar_atp_h thms =
    1.70      let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
    1.71          val prems' = map repeat_someI_ex prems
    1.72 @@ -112,7 +90,7 @@
    1.73  (* where N is the number of this subgoal                             *)
    1.74  (*********************************************************************)
    1.75  
    1.76 -fun tptp_inputs_tfrees thms n tfrees =
    1.77 +fun tptp_inputs_tfrees thms n tfrees axclauses =
    1.78      let
    1.79        val _ = debug ("in tptp_inputs_tfrees 0")
    1.80        val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.81 @@ -124,6 +102,7 @@
    1.82        val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
    1.83        val out = TextIO.openOut(probfile)
    1.84      in
    1.85 +      ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    1.86        ResLib.writeln_strs out (tfree_clss @ tptp_clss);
    1.87        TextIO.closeOut out;
    1.88        debug probfile
    1.89 @@ -160,7 +139,6 @@
    1.90      val axfile = (File.platform_path axiom_file)
    1.91  
    1.92      val hypsfile = (File.platform_path hyps_file)
    1.93 -    val clasimpfile = (File.platform_path clasimp_file)
    1.94  
    1.95      fun make_atp_list [] sign n = []
    1.96        | make_atp_list ((sko_thm, sg_term)::xs) sign n =
    1.97 @@ -174,7 +152,7 @@
    1.98              val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
    1.99              val _ = debug ("prob file in call_resolve_tac is " ^ probfile)
   1.100            in
   1.101 -            if !SpassComm.spass
   1.102 +            if !spass
   1.103              then
   1.104                let val optionline = (*Custom SPASS options, or default?*)
   1.105  		      if !full_spass (*Auto mode: all SPASS inference rules*)
   1.106 @@ -186,7 +164,7 @@
   1.107                in 
   1.108                    ([("spass", thmstr, goalstring,
   1.109                       getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
   1.110 -                     optionline, clasimpfile, axfile, hypsfile, probfile)] @ 
   1.111 +                     optionline, axfile, hypsfile, probfile)] @ 
   1.112                    (make_atp_list xs sign (n+1)))
   1.113                end
   1.114              else if !vampire 
   1.115 @@ -194,14 +172,14 @@
   1.116                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
   1.117                in
   1.118                  ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000",
   1.119 -                   clasimpfile, axfile, hypsfile, probfile)] @
   1.120 +                   axfile, hypsfile, probfile)] @
   1.121                   (make_atp_list xs sign (n+1)))
   1.122                end
   1.123        	     else
   1.124               let val Eprover = ResLib.helper_path "E_HOME" "eproof"
   1.125                in
   1.126                  ([("E", thmstr, goalstring, Eprover, "--tptp-in -l5",
   1.127 -                   clasimpfile, axfile, hypsfile, probfile)] @
   1.128 +                   axfile, hypsfile, probfile)] @
   1.129                   (make_atp_list xs sign (n+1)))
   1.130                end
   1.131  
   1.132 @@ -228,11 +206,11 @@
   1.133       else
   1.134  	
   1.135       ( SELECT_GOAL
   1.136 -        (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
   1.137 +        (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
   1.138            METAHYPS(fn negs => 
   1.139 -            (if !SpassComm.spass 
   1.140 +            (if !spass 
   1.141               then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
   1.142 -             else tptp_inputs_tfrees (make_clauses negs) n tfrees;
   1.143 +             else tptp_inputs_tfrees (make_clauses negs) n tfrees axclauses;
   1.144               get_sko_thms tfrees sign sg_terms (childin, childout, pid) 
   1.145                            thm  (n -1) (negs::sko_thms) axclauses; 
   1.146               all_tac))]) n thm )
   1.147 @@ -297,9 +275,8 @@
   1.148  
   1.149        (*set up variables for writing out the clasimps to a tptp file*)
   1.150        val (clause_arr, num_of_clauses, axclauses) =
   1.151 -        ResClasimp.write_out_clasimp (File.platform_path clasimp_file) thy
   1.152 -          (hd prems) (*FIXME: hack!! need to do all prems*)
   1.153 -      val _ = debug ("clasimp_file is " ^ File.platform_path clasimp_file ^ " with " ^ (string_of_int num_of_clauses)^ " clauses")
   1.154 +        ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
   1.155 +      val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^ " clauses")
   1.156        val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr, num_of_clauses)
   1.157        val pid_string =
   1.158          string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
   1.159 @@ -355,9 +332,7 @@
   1.160  (** the Isar toplevel hook **)
   1.161  
   1.162  val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   1.163 -
   1.164    let
   1.165 -
   1.166      val proof = Toplevel.proof_of state
   1.167      val (ctxt, (_, goal)) = Proof.get_goal proof
   1.168          handle Proof.STATE _ => error "No goal present";