Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
authorquigley
Fri Sep 02 21:29:33 2005 +0200 (2005-09-02)
changeset 172358e55ad29b690
parent 17234 12a9393c5d77
child 17236 6edb84c661dd
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
recon_transfer_proof.ML to deal with the E theorem prover.
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Sep 02 17:55:24 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Sep 02 21:29:33 2005 +0200
     1.3 @@ -217,6 +217,26 @@
     1.4     end
     1.5      
     1.6  
     1.7 +fun get_axiom_names_E proofstr thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses  =
     1.8 +   let 
     1.9 +     (* not sure why this is necessary again, but seems to be *)
    1.10 +      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.11 +      val step_nums =get_linenums proofstr
    1.12 +  
    1.13 +     (***********************************************)
    1.14 +     (* here need to add the clauses from clause_arr*)
    1.15 +     (***********************************************)
    1.16 +  
    1.17 +      val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums 
    1.18 +      val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
    1.19 +  
    1.20 +      val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))                                                               
    1.21 +                         (concat clasimp_names)
    1.22 +      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    1.23 +   in
    1.24 +      clasimp_names
    1.25 +   end
    1.26 +
    1.27  (***********************************************)
    1.28  (* get axioms for reconstruction               *)
    1.29  (***********************************************)
    1.30 @@ -419,6 +439,46 @@
    1.31      end;
    1.32  
    1.33  
    1.34 +fun EString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
    1.35 + let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
    1.36 +               (" thmstring is: "^thmstring^"proofstr is: "^proofstr^
    1.37 +                "goalstr is: "^goalstring^" num of clauses is: "^
    1.38 +                (string_of_int num_of_clauses))
    1.39 +
    1.40 +    (***********************************)
    1.41 +    (* get vampire axiom names         *)
    1.42 +    (***********************************)
    1.43 +
    1.44 +     val (axiom_names) = get_axiom_names_E proofstr  thms clause_arr  num_of_clauses
    1.45 +     val ax_str = "Rules from clasimpset used in proof found by E: " ^
    1.46 +                  rules_to_string axiom_names
    1.47 +    in 
    1.48 +	 File.append(File.tmp_path (Path.basic "reconstrfile")) ("reconstring is: "^ax_str^"  "^goalstring);
    1.49 +         TextIO.output (toParent, ax_str^"\n");
    1.50 +	 TextIO.flushOut toParent;
    1.51 +	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
    1.52 +	 TextIO.flushOut toParent;
    1.53 +	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
    1.54 +	 TextIO.flushOut toParent;
    1.55 +
    1.56 +	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.57 +	(* Attempt to prevent several signals from turning up simultaneously *)
    1.58 +	 Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
    1.59 +    end
    1.60 +    handle _ => 
    1.61 +    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
    1.62 +    in 
    1.63 +	TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
    1.64 +	TextIO.flushOut toParent;
    1.65 +	 TextIO.output (toParent, thmstring^"\n");
    1.66 +	 TextIO.flushOut toParent;
    1.67 +	 TextIO.output (toParent, goalstring^"\n");
    1.68 +	 TextIO.flushOut toParent;
    1.69 +	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.70 +	(* Attempt to prevent several signals from turning up simultaneously *)
    1.71 +	Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
    1.72 +    end;
    1.73 +
    1.74  (* val proofstr = "1582[0:Inp] || -> v_P*.\
    1.75                   \1583[0:Inp] || v_P* -> .\
    1.76  		 \1584[0:MRR:1583.0,1582.0] || -> ."; *)
     2.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Sep 02 17:55:24 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Sep 02 21:29:33 2005 +0200
     2.3 @@ -502,7 +502,8 @@
     2.4  				("subgoals forked to checkChildren:"^
     2.5  				prems_string^prover^thmstring^goalstring^childCmd) 
     2.6  			 val childDone = (case prover of
     2.7 -			     "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )                                              
     2.8 +			     "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )     
     2.9 +                              | "E" => (EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) )              
    2.10  			    |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
    2.11  		      in
    2.12  		       if childDone      (**********************************************)
     3.1 --- a/src/HOL/Tools/res_atp.ML	Fri Sep 02 17:55:24 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Sep 02 21:29:33 2005 +0200
     3.3 @@ -189,13 +189,22 @@
     3.4                       optionline, clasimpfile, axfile, hypsfile, probfile)] @ 
     3.5                    (make_atp_list xs sign (n+1)))
     3.6                end
     3.7 -            else
     3.8 +            else if !vampire 
     3.9 +	    then 
    3.10                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
    3.11                in
    3.12                  ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000",
    3.13                     clasimpfile, axfile, hypsfile, probfile)] @
    3.14                   (make_atp_list xs sign (n+1)))
    3.15                end
    3.16 +      	     else
    3.17 +             let val Eprover = ResLib.helper_path "E_HOME" "eproof"
    3.18 +              in
    3.19 +                ([("E", thmstr, goalstring, Eprover, "--tptp-in -l5",
    3.20 +                   clasimpfile, axfile, hypsfile, probfile)] @
    3.21 +                 (make_atp_list xs sign (n+1)))
    3.22 +              end
    3.23 +
    3.24            end
    3.25  
    3.26      val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1