# HG changeset patch # User blanchet # Date 1314018165 -7200 # Node ID 20bd9f90accc37935e7b286b0a04e323dc6c2101 # Parent 23adec5984f1927f6406c4d39047b4f6993b8a9f added option to control soundness of encodings more precisely, for evaluation purposes diff -r 23adec5984f1 -r 20bd9f90accc src/HOL/TPTP/atp_export.ML --- a/src/HOL/TPTP/atp_export.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/TPTP/atp_export.ML Mon Aug 22 15:02:45 2011 +0200 @@ -159,7 +159,7 @@ val (atp_problem, _, _, _, _, _, _) = facts |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th)) - |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true + |> prepare_atp_problem ctxt format Axiom Axiom type_enc Sound true combinatorsN false true [] @{prop False} val atp_problem = atp_problem diff -r 23adec5984f1 -r 20bd9f90accc src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 @@ -31,6 +31,8 @@ Guards of polymorphism * type_level * type_heaviness | Tags of polymorphism * type_level * type_heaviness + datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound + val no_lambdasN : string val concealedN : string val liftingN : string @@ -96,8 +98,8 @@ val helper_table : ((string * bool) * thm list) list val factsN : string val prepare_atp_problem : - Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool - -> bool -> string -> bool -> bool -> term list -> term + Proof.context -> format -> formula_kind -> formula_kind -> type_enc + -> soundness -> bool -> string -> bool -> bool -> term list -> term -> ((string * locality) * term) list -> string problem * string Symtab.table * int * int * (string * locality) list vector * int list * int Symtab.table @@ -622,6 +624,9 @@ | _ => type_enc) | format => (format, type_enc)) +(* Soundness controls how sound the "quasi-sound" encodings should be. *) +datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound + fun lift_lambdas ctxt type_enc = map (close_form o Envir.eta_contract) #> rpair ctxt #-> Lambda_Lifting.lift_lambdas @@ -1770,7 +1775,7 @@ (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it out with monotonicity" paper presented at CADE 2011. *) fun add_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I - | add_iterm_nonmonotonic_types ctxt level sound locality _ + | add_iterm_nonmonotonic_types ctxt level soundness locality _ (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) = (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso (case level of @@ -1779,22 +1784,25 @@ (* Unlike virtually any other polymorphic fact whose type variables can be instantiated by a known infinite type, extensionality actually encodes a cardinality constraints. *) - not (not sound andalso + not (soundness <> Sound andalso is_type_surely_infinite ctxt - (if locality = Extensionality then [] - else known_infinite_types) T) + (if locality = Extensionality orelse + soundness = Sound_Modulo_Infiniteness then + [] + else + known_infinite_types) T) | Fin_Nonmono_Types => is_type_surely_finite ctxt T | _ => true)) ? insert_type ctxt I (deep_freeze_type T) | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I -fun add_fact_nonmonotonic_types ctxt level sound +fun add_fact_nonmonotonic_types ctxt level soundness ({kind, locality, iformula, ...} : translated_formula) = formula_fold (SOME (kind <> Conjecture)) - (add_iterm_nonmonotonic_types ctxt level sound locality) + (add_iterm_nonmonotonic_types ctxt level soundness locality) iformula -fun nonmonotonic_types_for_facts ctxt type_enc sound facts = +fun nonmonotonic_types_for_facts ctxt type_enc soundness facts = let val level = level_of_type_enc type_enc in if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then - [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts + [] |> fold (add_fact_nonmonotonic_types ctxt level soundness) facts (* We must add "bool" in case the helper "True_or_False" is added later. In addition, several places in the code rely on the list of nonmonotonic types not being empty. (FIXME?) *) @@ -1972,7 +1980,7 @@ val explicit_apply = NONE (* for experiments *) -fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound +fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc soundness exporter lambda_trans readable_names preproc hyp_ts concl_t facts = let val (format, type_enc) = choose_format [format] type_enc @@ -2008,7 +2016,7 @@ hyp_ts concl_t facts val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply val nonmono_Ts = - conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound + conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc soundness val repair = repair_fact ctxt format type_enc sym_tab val (conjs, facts) = (conjs, facts) |> pairself (map repair) val repaired_sym_tab = diff -r 23adec5984f1 -r 20bd9f90accc src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Aug 22 15:02:45 2011 +0200 @@ -196,7 +196,7 @@ tracing ("PROPS:\n" ^ cat_lines (map (Syntax.string_of_term ctxt) props)) *) val (atp_problem, _, _, _, _, _, sym_tab) = - prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false + prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc Sound false no_lambdasN false false [] @{prop False} props (* val _ = tracing ("ATP PROBLEM: " ^ diff -r 23adec5984f1 -r 20bd9f90accc src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Aug 22 15:02:45 2011 +0200 @@ -65,6 +65,7 @@ val measure_run_time : bool Config.T val atp_lambda_translation : string Config.T val atp_readable_names : bool Config.T + val atp_sound_modulo_infiniteness : bool Config.T val smt_triggers : bool Config.T val smt_weights : bool Config.T val smt_weight_min_facts : int Config.T @@ -341,10 +342,13 @@ Attrib.setup_config_string @{binding sledgehammer_atp_lambda_translation} (K smartN) (* In addition to being easier to read, readable names are often much shorter, - especially if types are mangled in names. For these reason, they are enabled - by default. *) + especially if types are mangled in names. This makes a difference for some + provers (e.g., E). For these reason, short names are enabled by default. *) val atp_readable_names = Attrib.setup_config_bool @{binding sledgehammer_atp_readable_names} (K true) +val atp_sound_modulo_infiniteness = + Attrib.setup_config_bool @{binding sledgehammer_atp_sound_modulo_infiniteness} + (K true) val smt_triggers = Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true) @@ -642,10 +646,18 @@ |> Output.urgent_message else () + val soundness = + if sound then + if Config.get ctxt atp_sound_modulo_infiniteness then + Sound_Modulo_Infiniteness + else + Sound + else + Unsound val (atp_problem, pool, conjecture_offset, facts_offset, fact_names, typed_helpers, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind - type_enc sound false + type_enc soundness false (Config.get ctxt atp_lambda_translation) (Config.get ctxt atp_readable_names) true hyp_ts concl_t facts