--- 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\<emdash>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
--- 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)
--- 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