--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Jun 02 15:10:18 2014 +0200
@@ -651,10 +651,10 @@
(override_params prover type_enc (my_timeout time_slice)) fact_override
in
if !meth = "sledgehammer_tac" then
- sledge_tac 0.2 ATP_Systems.vampireN "mono_native"
- ORELSE' sledge_tac 0.2 ATP_Systems.eN "poly_guards??"
- ORELSE' sledge_tac 0.2 ATP_Systems.spassN "mono_native"
- ORELSE' sledge_tac 0.2 ATP_Systems.z3_tptpN "poly_tags??"
+ sledge_tac 0.2 ATP_Proof.vampireN "mono_native"
+ ORELSE' sledge_tac 0.2 ATP_Proof.eN "poly_guards??"
+ ORELSE' sledge_tac 0.2 ATP_Proof.spassN "mono_native"
+ ORELSE' sledge_tac 0.2 ATP_Proof.z3_tptpN "poly_tags??"
ORELSE' SMT_Solver.smt_tac ctxt thms
else if !meth = "smt" then
SMT_Solver.smt_tac ctxt thms
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Mon Jun 02 15:10:18 2014 +0200
@@ -89,7 +89,7 @@
else
()
-val default_prover = ATP_Systems.eN (* arbitrary ATP *)
+val default_prover = ATP_Proof.eN (* arbitrary ATP *)
fun with_index (i, s) = s ^ "@" ^ string_of_int i
--- a/src/HOL/TPTP/atp_problem_import.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Mon Jun 02 15:10:18 2014 +0200
@@ -209,18 +209,18 @@
else ""))
(atp_tac ctxt completeness [] (mult * timeout div frac) prover i)
in
- slice 2 0 ATP_Systems.spassN
- ORELSE slice 2 0 ATP_Systems.vampireN
- ORELSE slice 2 0 ATP_Systems.eN
- ORELSE slice 2 0 ATP_Systems.z3_tptpN
- ORELSE slice 1 1 ATP_Systems.spassN
- ORELSE slice 1 2 ATP_Systems.eN
- ORELSE slice 1 1 ATP_Systems.vampireN
- ORELSE slice 1 2 ATP_Systems.vampireN
+ slice 2 0 ATP_Proof.spassN
+ ORELSE slice 2 0 ATP_Proof.vampireN
+ ORELSE slice 2 0 ATP_Proof.eN
+ ORELSE slice 2 0 ATP_Proof.z3_tptpN
+ ORELSE slice 1 1 ATP_Proof.spassN
+ ORELSE slice 1 2 ATP_Proof.eN
+ ORELSE slice 1 1 ATP_Proof.vampireN
+ ORELSE slice 1 2 ATP_Proof.vampireN
ORELSE
(if demo then
- slice 2 0 ATP_Systems.satallaxN
- ORELSE slice 2 0 ATP_Systems.leo2N
+ slice 2 0 ATP_Proof.satallaxN
+ ORELSE slice 2 0 ATP_Proof.leo2N
else
no_tac)
end
@@ -238,7 +238,7 @@
ORELSE SOLVE_TIMEOUT (timeout div 10) "blast" (blast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 5) "auto+spass"
(auto_tac ctxt
- THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) ATP_Systems.spassN))
+ THEN ALLGOALS (atp_tac ctxt 0 [] (timeout div 5) ATP_Proof.spassN))
ORELSE SOLVE_TIMEOUT (timeout div 10) "fast" (fast_tac ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "z3" (smt_solver_tac "z3" ctxt i)
ORELSE SOLVE_TIMEOUT (timeout div 20) "cvc3" (smt_solver_tac "cvc3" ctxt i)
@@ -286,7 +286,7 @@
read_tptp_file thy (freeze_problem_consts thy o snd) file_name
val conj = make_conj assms conjs
val (last_hope_atp, last_hope_completeness) =
- if demo then (ATP_Systems.satallaxN, 0) else (ATP_Systems.vampireN, 2)
+ if demo then (ATP_Proof.satallaxN, 0) else (ATP_Proof.vampireN, 2)
in
(can_tac ctxt (auto_etc_tac ctxt (timeout div 2) 1) conj orelse
can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
--- a/src/HOL/Tools/ATP/atp_proof.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Jun 02 15:10:18 2014 +0200
@@ -41,6 +41,28 @@
type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list
+ (* Named ATPs *)
+ val agsyholN : string
+ val alt_ergoN : string
+ val dummy_thfN : string
+ val eN : string
+ val e_malesN : string
+ val e_parN : string
+ val e_sineN : string
+ val e_tofofN : string
+ val iproverN : string
+ val iprover_eqN : string
+ val leo2N : string
+ val satallaxN : string
+ val snarkN : string
+ val spassN : string
+ val spass_pirateN : string
+ val vampireN : string
+ val waldmeisterN : string
+ val z3_tptpN : string
+ val zipperpositionN : string
+ val remote_prefix : string
+
val agsyhol_core_rule : string
val satallax_core_rule : string
val spass_input_rule : string
@@ -59,7 +81,7 @@
val scan_general_id : string list -> string * string list
val parse_formula : string list ->
(string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list
- val atp_proof_of_tstplike_proof : string atp_problem -> string -> string atp_proof
+ val atp_proof_of_tstplike_proof : string -> string atp_problem -> string -> string atp_proof
val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof
val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof
val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof
@@ -71,6 +93,30 @@
open ATP_Util
open ATP_Problem
+(* Named ATPs *)
+
+val agsyholN = "agsyhol"
+val alt_ergoN = "alt_ergo"
+val dummy_thfN = "dummy_thf" (* for experiments *)
+val eN = "e"
+val e_malesN = "e_males"
+val e_parN = "e_par"
+val e_sineN = "e_sine"
+val e_tofofN = "e_tofof"
+val iproverN = "iprover"
+val iprover_eqN = "iprover_eq"
+val leo2N = "leo2"
+val satallaxN = "satallax"
+val snarkN = "snark"
+val spassN = "spass"
+val spass_pirateN = "spass_pirate"
+val vampireN = "vampire"
+val waldmeisterN = "waldmeister"
+val z3_tptpN = "z3_tptp"
+val zipperpositionN = "zipperposition"
+val remote_prefix = "remote_"
+
+
val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
val satallax_core_rule = "__satallax_core" (* arbitrary *)
val spass_input_rule = "Inp"
@@ -251,7 +297,8 @@
(Scan.repeat (Scan.option ($$ ",") |-- parse_dependency) >> flat) x
and parse_file_source x =
(Scan.this_string "file" |-- $$ "(" |-- scan_general_id
- -- Scan.option ($$ "," |-- scan_general_id) --| $$ ")") x
+ -- Scan.option ($$ "," |-- scan_general_id
+ --| Scan.option ($$"," |-- $$"[" -- Scan.option scan_general_id --| $$"]") --| $$ ")")) x
and parse_inference_source x =
(Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
--| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
@@ -506,14 +553,18 @@
(Scan.this_string "SZS core" |-- Scan.repeat ($$ " " |-- scan_general_id)
>> map (core_inference z3_tptp_core_rule)) x
-fun parse_line problem =
- parse_tstp_line problem || parse_z3_tptp_core_line || parse_spass_line || parse_spass_pirate_line
- || parse_satallax_core_line
-fun parse_proof problem =
+fun parse_line name problem =
+ if name = z3_tptpN then parse_z3_tptp_core_line
+ else if name = spass_pirateN then parse_spass_pirate_line
+ else if name = spassN then parse_spass_line
+ else if name = satallaxN then parse_satallax_core_line
+ else parse_tstp_line problem
+
+fun parse_proof name problem =
strip_spaces_except_between_idents
#> raw_explode
#> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
- (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line problem) >> flat)))
+ (Scan.finite Symbol.stopper (Scan.repeat1 (parse_line name problem) >> flat)))
#> fst
fun core_of_agsyhol_proof s =
@@ -522,14 +573,15 @@
_ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
| _ => NONE)
-fun atp_proof_of_tstplike_proof _ "" = []
- | atp_proof_of_tstplike_proof problem tstp =
+fun atp_proof_of_tstplike_proof prover _ "" = []
+ | atp_proof_of_tstplike_proof prover problem tstp =
(case core_of_agsyhol_proof tstp of
SOME facts => facts |> map (core_inference agsyhol_core_rule)
| NONE =>
tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
- |> parse_proof problem
- |> perhaps (try (sort (vampire_step_name_ord o pairself #1))))
+ |> parse_proof prover problem
+ |> prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1)))
+ |> prover = zipperpositionN ? rev)
fun clean_up_dependencies _ [] = []
| clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 02 15:10:18 2014 +0200
@@ -48,25 +48,6 @@
val spass_H2NuVS0Red2 : string
val spass_H2SOS : string
val spass_extra_options : string Config.T
- val agsyholN : string
- val alt_ergoN : string
- val dummy_thfN : string
- val eN : string
- val e_malesN : string
- val e_parN : string
- val e_sineN : string
- val e_tofofN : string
- val iproverN : string
- val iprover_eqN : string
- val leo2N : string
- val satallaxN : string
- val snarkN : string
- val spassN : string
- val spass_pirateN : string
- val vampireN : string
- val waldmeisterN : string
- val z3_tptpN : string
- val remote_prefix : string
val remote_atp :
string -> string -> string list -> (string * string) list
-> (atp_failure * string) list -> atp_formula_role
@@ -157,28 +138,6 @@
val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
val known_says_failures = known_szs_failures (prefix " says ")
-(* named ATPs *)
-
-val agsyholN = "agsyhol"
-val alt_ergoN = "alt_ergo"
-val dummy_thfN = "dummy_thf" (* for experiments *)
-val eN = "e"
-val e_malesN = "e_males"
-val e_parN = "e_par"
-val e_sineN = "e_sine"
-val e_tofofN = "e_tofof"
-val iproverN = "iprover"
-val iprover_eqN = "iprover_eq"
-val leo2N = "leo2"
-val satallaxN = "satallax"
-val snarkN = "snark"
-val spassN = "spass"
-val spass_pirateN = "spass_pirate"
-val vampireN = "vampire"
-val waldmeisterN = "waldmeister"
-val z3_tptpN = "z3_tptp"
-val remote_prefix = "remote_"
-
structure Data = Theory_Data
(
type T = ((unit -> atp_config) * stamp) Symtab.table
@@ -634,6 +593,27 @@
val z3_tptp = (z3_tptpN, fn () => z3_tptp_config)
+(* Zipperposition*)
+
+val zipperposition_tff1 = TFF Polymorphic
+
+val zipperposition_config : atp_config =
+ {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
+ arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
+ "-print none -proof tstp -print-types -timeout " ^
+ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
+ proof_delims = tstp_proof_delims,
+ known_failures = known_szs_status_failures,
+ prem_role = Hypothesis,
+ best_slices = fn _ =>
+ (* FUDGE *)
+ [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))],
+ best_max_mono_iters = default_max_mono_iters,
+ best_max_new_mono_instances = default_max_new_mono_instances}
+
+val zipperposition = (zipperpositionN, fn () => zipperposition_config)
+
+
(* Not really a prover: Experimental Polymorphic THF and DFG output *)
fun dummy_config prem_role format type_enc uncurried_aliases : atp_config =
@@ -816,8 +796,8 @@
val atps =
[agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
- z3_tptp, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof, remote_iprover,
- remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
+ z3_tptp,zipperposition, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof,
+ remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
remote_spass_pirate, remote_waldmeister]
val setup = fold add_atp atps
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jun 02 15:10:18 2014 +0200
@@ -18,6 +18,7 @@
open ATP_Util
open ATP_Systems
open ATP_Problem_Generate
+open ATP_Proof
open ATP_Proof_Reconstruct
open Sledgehammer_Util
open Sledgehammer_Fact
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Jun 02 15:10:18 2014 +0200
@@ -123,8 +123,8 @@
fun isar_proof_of () =
let
- val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
- atp_proof, goal) = try isar_params ()
+ val (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize,
+ atp_proof, goal) = isar_params ()
val systematic_methods = insert (op =) (Metis_Method alt_metis_args) systematic_methods0
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Jun 02 15:10:18 2014 +0200
@@ -122,7 +122,7 @@
fun chain_qs_lfs NONE lfs = ([], lfs)
| chain_qs_lfs (SOME l0) lfs =
if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
-fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
+fun chain_isar_step lbl (x as Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
let val (qs', lfs) = chain_qs_lfs lbl lfs in
Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Jun 02 15:10:18 2014 +0200
@@ -95,9 +95,10 @@
structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER =
struct
+open ATP_Proof
open ATP_Util
+open ATP_Systems
open ATP_Problem
-open ATP_Systems
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Metis_Tactic
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 02 14:29:20 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Jun 02 15:10:18 2014 +0200
@@ -287,7 +287,7 @@
|> (fn accum as (output, _) =>
(accum,
extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
- |>> atp_proof_of_tstplike_proof atp_problem
+ |>> atp_proof_of_tstplike_proof name atp_problem
handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
val outcome =