# HG changeset patch
# User fleury
# Date 1406721792 -7200
# Node ID 9cda0c64c37aa9fe1e229056a966e1454c1740c3
# Parent  4b52c1b319ced0b3399f4f41cd4b97875c096c61
imported patch hilbert_choice_support

diff -r 4b52c1b319ce -r 9cda0c64c37a src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/ATP.thy	Wed Jul 30 14:03:12 2014 +0200
@@ -6,7 +6,7 @@
 header {* Automatic Theorem Provers (ATPs) *}
 
 theory ATP
-imports Meson
+imports Meson Hilbert_Choice
 begin
 
 subsection {* ATP problems and proofs *}
diff -r 4b52c1b319ce -r 9cda0c64c37a src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -76,6 +76,8 @@
   val tptp_ho_exists : string
   val tptp_choice : string
   val tptp_ho_choice : string
+  val tptp_hilbert_choice : string
+  val tptp_hilbert_the : string
   val tptp_not : string
   val tptp_and : string
   val tptp_not_and : string
@@ -239,6 +241,8 @@
 val tptp_iff = "<=>"
 val tptp_not_iff = "<~>"
 val tptp_app = "@"
+val tptp_hilbert_choice = "@+"
+val tptp_hilbert_the = "@-"
 val tptp_not_infix = "!"
 val tptp_equal = "="
 val tptp_not_equal = "!="
diff -r 4b52c1b319ce -r 9cda0c64c37a src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -478,10 +478,19 @@
   [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
    tptp_equal, tptp_app]
 
+fun parse_one_in_list list =
+  foldl1 (op ||) (map Scan.this_string list)
+
 fun parse_binary_op x =
-  (foldl1 (op ||) (map Scan.this_string tptp_binary_ops)
+  (parse_one_in_list tptp_binary_ops
    >> (fn c => if c = tptp_equal then "equal" else c)) x
 
+val parse_fo_quantifier =
+   parse_one_in_list [tptp_forall, tptp_exists, tptp_lambda, tptp_hilbert_choice, tptp_hilbert_the]
+
+val parse_ho_quantifier =
+   parse_one_in_list [tptp_ho_forall, tptp_ho_exists, tptp_hilbert_choice, tptp_hilbert_the]
+
 fun parse_thf0_type x =
   (($$ "(" |-- parse_thf0_type --| $$ ")" || scan_general_id >> (fn t => AType ((t, []), [])))
    -- Scan.option ($$ tptp_fun_type |-- parse_thf0_type)
@@ -491,6 +500,8 @@
 fun mk_ho_of_fo_quant q =
   if q = tptp_forall then tptp_ho_forall
   else if q = tptp_exists then tptp_ho_exists
+  else if q = tptp_hilbert_choice then tptp_hilbert_choice
+  else if q = tptp_hilbert_the then tptp_hilbert_the
   else raise Fail ("unrecognized quantification: " ^ q)
 
 fun remove_thf_app (ATerm ((x, ty), arg)) =
@@ -508,8 +519,7 @@
    || $$ "(" |-- parse_thf0_typed_var --| $$ ")") x
 
 fun parse_simple_thf0_term x =
-  ((Scan.this_string tptp_forall || Scan.this_string tptp_exists || Scan.this_string tptp_lambda)
-        -- ($$ "[" |-- parse_thf0_typed_var --| $$ "]" --| $$ ":") -- parse_thf0_term
+  (parse_fo_quantifier -- ($$ "[" |-- parse_thf0_typed_var --| $$ "]" --| $$ ":") -- parse_thf0_term
       >> (fn ((q, ys), t) =>
           fold_rev
             (fn (var, ty) => fn r =>
@@ -521,7 +531,7 @@
             ys t)
   || Scan.this_string tptp_not |-- parse_thf0_term >> mk_app (mk_simple_aterm tptp_not)
   || scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var, typ) => ATerm ((var, [typ]), []))
-  || (Scan.this_string tptp_ho_forall || Scan.this_string tptp_ho_exists) >> mk_simple_aterm
+  || parse_ho_quantifier >> mk_simple_aterm
   || $$ "(" |-- parse_thf0_term --| $$ ")"
   || scan_general_id >> mk_simple_aterm) x
 and parse_thf0_term x =
diff -r 4b52c1b319ce -r 9cda0c64c37a src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -269,6 +269,8 @@
         else if s = tptp_not then HOLogic.Not
         else if s = tptp_ho_forall then HOLogic.all_const dummyT
         else if s = tptp_ho_exists then HOLogic.exists_const dummyT
+        else if s = tptp_hilbert_choice then HOLogic.choice_const dummyT
+        else if s = tptp_hilbert_the then @{term "The"}
         else
           (case unprefix_and_unascii const_prefix s of
             SOME s' =>
diff -r 4b52c1b319ce -r 9cda0c64c37a src/HOL/Tools/SMT2/smt2_systems.ML
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -103,8 +103,9 @@
     "--disable-banner",
     "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]),
   smt_options = [],
-  default_max_relevant = 250 (* FUDGE *),
-  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "warning : proof_done: status is still open"),
+  default_max_relevant = 120 (* FUDGE *),
+  outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
+              "warning : proof_done: status is still open"),
   parse_proof = SOME VeriT_Proof_Parse.parse_proof,
   replay = NONE }
 
diff -r 4b52c1b319ce -r 9cda0c64c37a src/HOL/Tools/SMT2/verit_proof.ML
--- a/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_proof.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -306,7 +306,7 @@
          {fix sk ....}
          hence "..sk.."
          thus "(if ..)"
-      last step does not work: the step before is buggy. Without the proof work.*)
+      last step does not work: the step before is buggy. Without it, the proof work.*)
         mk_node id veriT_tmp_skolemize (if null prems then [mk_string_id (~num_of_steps - id)]
           else prems) concl' []
       end
diff -r 4b52c1b319ce -r 9cda0c64c37a src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:12 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 30 14:03:12 2014 +0200
@@ -48,6 +48,7 @@
 
 val e_skolemize_rule = "skolemize"
 val leo2_extcnf_combined_rule = "extcnf_combined"
+val satallax_skolemize_rule = "tab_ex"
 val spass_pirate_datatype_rule = "DT"
 val vampire_skolemisation_rule = "skolemisation"
 val veriT_tmp_skolemize_rule = "tmp_skolemize"
@@ -61,7 +62,8 @@
 
 val skolemize_rules =
   [e_skolemize_rule, spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule,
-zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_tmp_skolemize_rule]
+zipperposition_cnf_rule, leo2_extcnf_combined_rule, veriT_tmp_skolemize_rule,
+satallax_skolemize_rule]
 
 val is_skolemize_rule = member (op =) skolemize_rules
 val is_arith_rule = (String.isPrefix z3_th_lemma_rule) orf (member (op =) veriT_arith_rules)