# HG changeset patch
# User blanchet
# Date 1406914330 -7200
# Node ID d7454ee84f348b5181783ab505b90d67bb2ff98a
# Parent  b2e6166bf4874320a5385f22a006097f5862f374
more precise handling of LEO-II skolemization

diff -r b2e6166bf487 -r d7454ee84f34 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Aug 01 16:07:34 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Aug 01 19:32:10 2014 +0200
@@ -397,17 +397,16 @@
 
 (* LEO-II *)
 
-(* LEO-II supports definitions, but it performs significantly better on our
-   benchmarks when they are not used. *)
 val leo2_thf0 = THF (Monomorphic, THF_Without_Choice)
 
 val leo2_config : atp_config =
   {exec = K (["LEO2_HOME"], ["leo.opt", "leo"]),
-   arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
-       "--foatp e --atp e=\"$E_HOME\"/eprover \
-       \--atp epclextract=\"$E_HOME\"/epclextract \
-       \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
-       file_name,
+   arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ =>
+     "--foatp e --atp e=\"$E_HOME\"/eprover \
+     \--atp epclextract=\"$E_HOME\"/epclextract \
+     \--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout) ^ " " ^
+     (if full_proofs then "--notReplLeibnizEQ --notReplAndrewsEQ --notUseExtCnfCmbd " else "") ^
+     file_name,
    proof_delims = tstp_proof_delims,
    known_failures =
      [(TimedOut, "CPU time limit exceeded, terminating"),
diff -r b2e6166bf487 -r d7454ee84f34 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 16:07:34 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Aug 01 19:32:10 2014 +0200
@@ -47,7 +47,7 @@
 val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false)
 
 val e_skolemize_rule = "skolemize"
-val leo2_extcnf_combined_rule = "extcnf_combined"
+val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg"
 val satallax_skolemize_rule = "tab_ex"
 val spass_pirate_datatype_rule = "DT"
 val vampire_skolemisation_rule = "skolemisation"
@@ -61,10 +61,8 @@
 val z3_th_lemma_rule = "th-lemma"
 val zipperposition_cnf_rule = "cnf"
 
-(* Unfortunately, LEO-II's "extcnf_combined" rule captures clausification in general and not only
-   skolemization. *)
 val skolemize_rules =
-  [e_skolemize_rule, leo2_extcnf_combined_rule, satallax_skolemize_rule, spass_skolemize_rule,
+  [e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, spass_skolemize_rule,
    vampire_skolemisation_rule, veriT_tmp_ite_elim_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule,
    zipperposition_cnf_rule]