* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
1.1 --- a/NEWS Mon Apr 07 15:37:04 2008 +0200
1.2 +++ b/NEWS Mon Apr 07 15:37:27 2008 +0200
1.3 @@ -173,6 +173,8 @@
1.4 * Metis prover is now an order of magnitude faster, and also works
1.5 with multithreading.
1.6
1.7 +* Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
1.8 +
1.9 * Sledgehammer no longer produces structured proofs by default. To enable,
1.10 declare [[sledgehammer_full = true]]. Attributes reconstruction_modulus,
1.11 reconstruction_sorts renamed sledgehammer_modulus, sledgehammer_sorts.
2.1 --- a/src/HOL/Hilbert_Choice.thy Mon Apr 07 15:37:04 2008 +0200
2.2 +++ b/src/HOL/Hilbert_Choice.thy Mon Apr 07 15:37:27 2008 +0200
2.3 @@ -635,6 +635,8 @@
2.4
2.5 use "Tools/meson.ML"
2.6
2.7 +setup Meson.setup
2.8 +
2.9
2.10 subsection {* Specification package -- Hilbertized version *}
2.11
3.1 --- a/src/HOL/Tools/meson.ML Mon Apr 07 15:37:04 2008 +0200
3.2 +++ b/src/HOL/Tools/meson.ML Mon Apr 07 15:37:27 2008 +0200
3.3 @@ -14,7 +14,7 @@
3.4 val first_order_resolve: thm -> thm -> thm
3.5 val flexflex_first_order: thm -> thm
3.6 val size_of_subgoals: thm -> int
3.7 - val too_many_clauses: term -> bool
3.8 + val too_many_clauses: Proof.context option -> term -> bool
3.9 val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
3.10 val finish_cnf: thm list -> thm list
3.11 val make_nnf: thm -> thm
3.12 @@ -41,11 +41,15 @@
3.13 val negate_head: thm -> thm
3.14 val select_literal: int -> thm -> thm
3.15 val skolemize_tac: int -> tactic
3.16 + val setup: Context.theory -> Context.theory
3.17 end
3.18
3.19 structure Meson: MESON =
3.20 struct
3.21
3.22 +val max_clauses_default = 60;
3.23 +val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
3.24 +
3.25 val not_conjD = thm "meson_not_conjD";
3.26 val not_disjD = thm "meson_not_disjD";
3.27 val not_notD = thm "meson_not_notD";
3.28 @@ -237,37 +241,39 @@
3.29
3.30 (*** The basic CNF transformation ***)
3.31
3.32 -val max_clauses = 40;
3.33 -
3.34 -fun sum x y = if x < max_clauses andalso y < max_clauses then x+y else max_clauses;
3.35 -fun prod x y = if x < max_clauses andalso y < max_clauses then x*y else max_clauses;
3.36 -
3.37 -(*Estimate the number of clauses in order to detect infeasible theorems*)
3.38 -fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
3.39 - | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
3.40 - | signed_nclauses b (Const("op &",_) $ t $ u) =
3.41 - if b then sum (signed_nclauses b t) (signed_nclauses b u)
3.42 - else prod (signed_nclauses b t) (signed_nclauses b u)
3.43 - | signed_nclauses b (Const("op |",_) $ t $ u) =
3.44 - if b then prod (signed_nclauses b t) (signed_nclauses b u)
3.45 - else sum (signed_nclauses b t) (signed_nclauses b u)
3.46 - | signed_nclauses b (Const("op -->",_) $ t $ u) =
3.47 - if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
3.48 - else sum (signed_nclauses (not b) t) (signed_nclauses b u)
3.49 - | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
3.50 - if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
3.51 - if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
3.52 - (prod (signed_nclauses (not b) u) (signed_nclauses b t))
3.53 - else sum (prod (signed_nclauses b t) (signed_nclauses b u))
3.54 - (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
3.55 - else 1
3.56 - | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
3.57 - | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
3.58 - | signed_nclauses _ _ = 1; (* literal *)
3.59 -
3.60 -val nclauses = signed_nclauses true;
3.61 -
3.62 -fun too_many_clauses t = nclauses t >= max_clauses;
3.63 +fun too_many_clauses ctxto t =
3.64 + let
3.65 + val max_cl = case ctxto of SOME ctxt => Config.get ctxt max_clauses
3.66 + | NONE => max_clauses_default
3.67 +
3.68 + fun sum x y = if x < max_cl andalso y < max_cl then x+y else max_cl;
3.69 + fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
3.70 +
3.71 + (*Estimate the number of clauses in order to detect infeasible theorems*)
3.72 + fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
3.73 + | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
3.74 + | signed_nclauses b (Const("op &",_) $ t $ u) =
3.75 + if b then sum (signed_nclauses b t) (signed_nclauses b u)
3.76 + else prod (signed_nclauses b t) (signed_nclauses b u)
3.77 + | signed_nclauses b (Const("op |",_) $ t $ u) =
3.78 + if b then prod (signed_nclauses b t) (signed_nclauses b u)
3.79 + else sum (signed_nclauses b t) (signed_nclauses b u)
3.80 + | signed_nclauses b (Const("op -->",_) $ t $ u) =
3.81 + if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
3.82 + else sum (signed_nclauses (not b) t) (signed_nclauses b u)
3.83 + | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
3.84 + if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
3.85 + if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
3.86 + (prod (signed_nclauses (not b) u) (signed_nclauses b t))
3.87 + else sum (prod (signed_nclauses b t) (signed_nclauses b u))
3.88 + (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
3.89 + else 1
3.90 + | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
3.91 + | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
3.92 + | signed_nclauses _ _ = 1; (* literal *)
3.93 + in
3.94 + signed_nclauses true t >= max_cl
3.95 + end;
3.96
3.97 (*Replaces universally quantified variables by FREE variables -- because
3.98 assumptions may not contain scheme variables. Later, generalize using Variable.export. *)
3.99 @@ -328,8 +334,8 @@
3.100 | _ => nodups th :: ths (*no work to do*)
3.101 and cnf_nil th = cnf_aux (th,[])
3.102 val cls =
3.103 - if too_many_clauses (concl_of th)
3.104 - then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
3.105 + if too_many_clauses (SOME ctxt) (concl_of th)
3.106 + then (warning ("cnf is ignoring: " ^ string_of_thm th); ths)
3.107 else cnf_aux (th,ths)
3.108 in (cls, !ctxtr) end;
3.109
4.1 --- a/src/HOL/Tools/res_axioms.ML Mon Apr 07 15:37:04 2008 +0200
4.2 +++ b/src/HOL/Tools/res_axioms.ML Mon Apr 07 15:37:27 2008 +0200
4.3 @@ -339,7 +339,7 @@
4.4
4.5 fun too_complex t =
4.6 apply_depth t > max_apply_depth orelse
4.7 - Meson.too_many_clauses t orelse
4.8 + Meson.too_many_clauses NONE t orelse
4.9 excessive_lambdas_fm [] t;
4.10
4.11 fun is_strange_thm th =