# 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)