wneuper/isa: src/HOL/Tools/atp_wrapper.ML@10eb446df3c7

     1 (*  Title:      HOL/Tools/atp_wrapper.ML

     2     Author:     Fabian Immler, TU Muenchen

     4 Wrapper functions for external ATPs.

     5 *)

     7 signature ATP_WRAPPER =

     8 sig

     9   val destdir: string ref

    10   val problem_name: string ref

    11   val external_prover:

    12     (thm * (string * int)) list ->

    13     (Path.T -> thm -> int -> (thm * (string * int)) list -> theory -> string vector) ->

    14     Path.T * string -> (string -> string option) ->

    15     (string * string vector * Proof.context * thm * int -> string) ->

    16     AtpManager.prover

    17   val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover

    18   val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover

    19   val tptp_prover: Path.T * string -> AtpManager.prover

    20   val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover

    21   val full_prover: Path.T * string  -> AtpManager.prover

    22   val vampire_opts: int -> bool -> AtpManager.prover

    23   val vampire: AtpManager.prover

    24   val vampire_opts_full: int -> bool -> AtpManager.prover

    25   val vampire_full: AtpManager.prover

    26   val eprover_opts: int -> bool  -> AtpManager.prover

    27   val eprover: AtpManager.prover

    28   val eprover_opts_full: int -> bool -> AtpManager.prover

    29   val eprover_full: AtpManager.prover

    30   val spass_opts: int -> bool  -> AtpManager.prover

    31   val spass: AtpManager.prover

    32   val remote_prover_opts: int -> bool -> string -> AtpManager.prover

    33   val remote_prover: string -> AtpManager.prover

    34 end;

    36 structure AtpWrapper: ATP_WRAPPER =

    37 struct

    39 (** generic ATP wrapper **)

    41 (* global hooks for writing problemfiles *)

    43 val destdir = ref "";   (*Empty means write files to /tmp*)

    44 val problem_name = ref "prob";

    47 (* basic template *)

    49 fun external_prover axiom_clauses write_problem_file (cmd, args) find_failure produce_answer timeout subgoalno goal =

    50   let

    51     (* path to unique problem file *)

    52     val destdir' = ! destdir

    53     val problem_name' = ! problem_name

    54     fun prob_pathname nr =

    55       let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)

    56       in if destdir' = "" then File.tmp_path probfile

    57         else if File.exists (Path.explode (destdir'))

    58         then Path.append  (Path.explode (destdir')) probfile

    59         else error ("No such directory: " ^ destdir')

    60       end

    62     (* write out problem file and call prover *)

    63     val (ctxt, (chain_ths, th)) = goal

    64     val thy = ProofContext.theory_of ctxt

    65     val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths

    66     val probfile = prob_pathname subgoalno

    67     val fname = File.platform_path probfile

    68     val thm_names = write_problem_file probfile th subgoalno axiom_clauses thy

    69     val cmdline =

    70       if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args

    71       else error ("Bad executable: " ^ Path.implode cmd)

    72     val (proof, rc) = system_out (cmdline ^ " " ^ fname)

    74     (* remove *temporary* files *)

    75     val _ = if destdir' = "" then OS.FileSys.remove fname else ()

    77     (* check for success and print out some information on failure *)

    78     val failure = find_failure proof

    79     val success = rc = 0 andalso is_none failure

    80     val message =

    81       if is_some failure then "External prover failed."

    82       else if rc <> 0 then "External prover failed: " ^ proof

    83       else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, th, subgoalno)

    85     val _ =

    86       if is_some failure

    87       then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)

    88       else ()

    89     val _ =

    90       if rc <> 0

    91       then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)

    92       else ()

    93   in (success, message) end;

    97 (** common provers **)

    99 (* generic TPTP-based provers *)

   101 fun tptp_prover_opts_full max_new theory_const full command timeout n goal =

   102   external_prover

   103     (ResAtp.get_relevant max_new theory_const goal n)

   104     (ResAtp.write_problem_file false)

   105     command

   106     ResReconstruct.find_failure

   107     (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)

   108     timeout n goal;

   110 (*arbitrary ATP with TPTP input/output and problemfile as last argument*)

   111 fun tptp_prover_opts max_new theory_const =

   112   tptp_prover_opts_full max_new theory_const false;

   114 val tptp_prover = tptp_prover_opts 60 true;

   116 (*for structured proofs: prover must support TSTP*)

   117 fun full_prover_opts max_new theory_const =

   118   tptp_prover_opts_full max_new theory_const true;

   120 val full_prover = full_prover_opts 60 true;

   123 (* Vampire *)

   125 (*NB: Vampire does not work without explicit timelimit*)

   127 fun vampire_opts max_new theory_const timeout = tptp_prover_opts

   128   max_new theory_const

   129   (Path.explode "$VAMPIRE_HOME/vampire",

   130                ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))

   131   timeout;

   133 val vampire = vampire_opts 60 false;

   135 fun vampire_opts_full max_new theory_const timeout = full_prover_opts

   136   max_new theory_const

   137   (Path.explode "$VAMPIRE_HOME/vampire",

   138                ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))

   139   timeout;

   141 val vampire_full = vampire_opts 60 false;

   144 (* E prover *)

   146 fun eprover_opts max_new theory_const timeout = tptp_prover_opts

   147   max_new theory_const

   148   (Path.explode "$E_HOME/eproof",

   149     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)

   150   timeout;

   152 val eprover = eprover_opts 100 false;

   154 fun eprover_opts_full max_new theory_const timeout = full_prover_opts

   155   max_new theory_const

   156   (Path.explode "$E_HOME/eproof",

   157     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)

   158   timeout;

   160 val eprover_full = eprover_opts_full 100 false;

   163 (* SPASS *)

   165 fun spass_opts max_new theory_const timeout n goal = external_prover

   166   (ResAtp.get_relevant max_new theory_const goal n)

   167   (ResAtp.write_problem_file true)

   168   (Path.explode "$SPASS_HOME/SPASS",

   169     "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)

   170   ResReconstruct.find_failure

   171   ResReconstruct.lemma_list_dfg

   172   timeout n goal;

   174 val spass = spass_opts 40 true;

   177 (* remote prover invocation via SystemOnTPTP *)

   179 fun remote_prover_opts max_new theory_const args timeout =

   180   tptp_prover_opts max_new theory_const

   181   (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP", args ^ " -t " ^ string_of_int timeout)

   182   timeout;

   184 val remote_prover = remote_prover_opts 60 false;

   186 end;

author	wenzelm
	Sat, 25 Apr 2009 20:31:27 +0200
changeset 30980	10eb446df3c7
parent 30899	d394a17d4fdb
child 31037	ac8669134e7a
permissions	-rw-r--r--