# HG changeset patch # User blanchet # Date 1335253660 -7200 # Node ID 39229c76063684d8e679cba44870385e9f36fc74 # Parent a0125644ccff578e285d34ffd6dea44ccc800553 smoother handling of conjecture, so that its Skolem constants get displayed in countermodels diff -r a0125644ccff -r 39229c760636 src/HOL/TPTP/atp_problem_import.ML --- a/src/HOL/TPTP/atp_problem_import.ML Tue Apr 24 09:47:40 2012 +0200 +++ b/src/HOL/TPTP/atp_problem_import.ML Tue Apr 24 09:47:40 2012 +0200 @@ -24,20 +24,16 @@ (** TPTP parsing based on ML-Yacc-generated "TPTP_Parser" **) -fun mk_meta_not P = Logic.mk_implies (P, @{prop False}) - (* cf. "close_form" in "refute.ML" *) fun close_form t = fold (fn ((s, i), T) => fn t' => Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) (Term.add_vars t []) t -fun get_tptp_formula (_, role, P, _) = - P |> Logic.varify_global |> close_form - |> role = TPTP_Syntax.Role_Conjecture ? mk_meta_not - fun read_tptp_file thy file_name = let + fun has_role role (_, role', _, _) = (role' = role) + fun get_prop (_, _, P, _) = P |> Logic.varify_global |> close_form val path = Path.explode file_name |> (fn path => @@ -45,12 +41,12 @@ ? Path.append (Path.explode "$PWD")) val ((_, _, problem), thy) = TPTP_Interpret.interpret_file true (Path.explode "$TPTP") path [] [] thy - val partitioned_problem = - List.partition (fn (_, role, _, _) => role = TPTP_Syntax.Role_Definition) - problem + val (conjs, defs_and_nondefs) = + problem |> List.partition (has_role TPTP_Syntax.Role_Conjecture) + ||> List.partition (has_role TPTP_Syntax.Role_Definition) in - (exists (fn (_, role, _, _) => role = TPTP_Syntax.Role_Conjecture) problem, - pairself (map get_tptp_formula) partitioned_problem, Theory.checkpoint thy) + (map get_prop conjs, pairself (map get_prop) defs_and_nondefs, + Theory.checkpoint thy) end (** Isabelle (combination of provers) **) @@ -60,11 +56,15 @@ (** Nitpick (alias Nitrox) **) +fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1 + | aptrueprop f t = f t + fun nitpick_tptp_file timeout file_name = let - val (falsify, (defs, nondefs), thy) = read_tptp_file @{theory} file_name + val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name val ctxt = Proof_Context.init_global thy - val defs = defs |> map (ATP_Util.extensionalize_term ctxt) + val defs = defs |> map (ATP_Util.extensionalize_term ctxt + #> aptrueprop (open_form I)) val state = Proof.init ctxt val params = [("card", "1\100"), @@ -72,14 +72,15 @@ ("sat_solver", "smart"), ("max_threads", "1"), ("batch_size", "10"), - ("falsify", if falsify then "true" else "false"), + ("falsify", if null conjs then "false" else "true"), (* ("debug", "true"), *) ("verbose", "true"), (* ("overlord", "true"), *) ("show_consts", "true"), ("format", "1000"), ("max_potential", "0"), - ("timeout", string_of_int timeout)] + ("timeout", string_of_int timeout), + ("tac_timeout", string_of_int ((timeout + 49) div 50))] |> Nitpick_Isar.default_params thy val i = 1 val n = 1 @@ -87,7 +88,8 @@ val subst = [] in Nitpick.pick_nits_in_term state params Nitpick.TPTP i n step subst - defs nondefs (if falsify then @{prop False} else @{prop True}); () + defs nondefs (case conjs of conj :: _ => conj | _ => @{prop True}); + () end @@ -103,14 +105,15 @@ fun refute_tptp_file timeout file_name = let - val (falsify, (defs, nondefs), thy) = read_tptp_file @{theory} file_name + val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name val ctxt = Proof_Context.init_global thy val params = [("maxtime", string_of_int timeout), ("maxvars", "100000")] in - Refute.refute_term ctxt params (defs @ nondefs) @{prop False} - |> print_szs_from_outcome falsify + Refute.refute_term ctxt params (defs @ nondefs) + (case conjs of conj :: _ => conj | _ => @{prop True}) + |> print_szs_from_outcome (not (null conjs)) end diff -r a0125644ccff -r 39229c760636 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Apr 24 09:47:40 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Apr 24 09:47:40 2012 +0200 @@ -764,18 +764,6 @@ (if String.isPrefix lam_lifted_prefix s then Const else Free) x | constify_lifted t = t -(* Requires bound variables not to clash with any schematic variables (as should - be the case right after lambda-lifting). *) -fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) = - (case try unprefix s of - SOME s => - let - val names = Name.make_context (map fst (Term.add_var_names t' [])) - val (s, _) = Name.variant s names - in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end - | NONE => t) - | open_form _ t = t - fun lift_lams_part_1 ctxt type_enc = map close_form #> rpair ctxt #-> Lambda_Lifting.lift_lambdas @@ -792,6 +780,8 @@ of them *) |> pairself (map (introduce_combinators ctxt)) |> pairself (map constify_lifted) + (* Requires bound variables not to clash with any schematic variables (as + should be the case right after lambda-lifting). *) |>> map (open_form (unprefix close_form_prefix)) ||> map (open_form I) diff -r a0125644ccff -r 39229c760636 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Tue Apr 24 09:47:40 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Tue Apr 24 09:47:40 2012 +0200 @@ -33,6 +33,7 @@ val s_iff : term * term -> term val close_form_prefix : string val close_form : term -> term + val open_form : (string -> string) -> term -> term val monomorphic_term : Type.tyenv -> term -> term val eta_expand : typ list -> term -> int -> term val extensionalize_term : Proof.context -> term -> term @@ -273,6 +274,16 @@ abstract_over (Var ((s, i), T), t'))) (Term.add_vars t []) t +fun open_form unprefix (t as Const (@{const_name All}, _) $ Abs (s, T, t')) = + (case try unprefix s of + SOME s => + let + val names = Name.make_context (map fst (Term.add_var_names t' [])) + val (s, _) = Name.variant s names + in open_form unprefix (subst_bound (Var ((s, 0), T), t')) end + | NONE => t) + | open_form _ t = t + fun monomorphic_term subst = map_types (map_type_tvar (fn v => case Type.lookup subst v of