1.1 --- a/src/HOL/Tools/meson.ML Mon Apr 07 15:37:04 2008 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Mon Apr 07 15:37:27 2008 +0200
1.3 @@ -14,7 +14,7 @@
1.4 val first_order_resolve: thm -> thm -> thm
1.5 val flexflex_first_order: thm -> thm
1.6 val size_of_subgoals: thm -> int
1.7 - val too_many_clauses: term -> bool
1.8 + val too_many_clauses: Proof.context option -> term -> bool
1.9 val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
1.10 val finish_cnf: thm list -> thm list
1.11 val make_nnf: thm -> thm
1.12 @@ -41,11 +41,15 @@
1.13 val negate_head: thm -> thm
1.14 val select_literal: int -> thm -> thm
1.15 val skolemize_tac: int -> tactic
1.16 + val setup: Context.theory -> Context.theory
1.17 end
1.18
1.19 structure Meson: MESON =
1.20 struct
1.21
1.22 +val max_clauses_default = 60;
1.23 +val (max_clauses, setup) = Attrib.config_int "max_clauses" max_clauses_default;
1.24 +
1.25 val not_conjD = thm "meson_not_conjD";
1.26 val not_disjD = thm "meson_not_disjD";
1.27 val not_notD = thm "meson_not_notD";
1.28 @@ -237,37 +241,39 @@
1.29
1.30 (*** The basic CNF transformation ***)
1.31
1.32 -val max_clauses = 40;
1.33 -
1.34 -fun sum x y = if x < max_clauses andalso y < max_clauses then x+y else max_clauses;
1.35 -fun prod x y = if x < max_clauses andalso y < max_clauses then x*y else max_clauses;
1.36 -
1.37 -(*Estimate the number of clauses in order to detect infeasible theorems*)
1.38 -fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
1.39 - | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
1.40 - | signed_nclauses b (Const("op &",_) $ t $ u) =
1.41 - if b then sum (signed_nclauses b t) (signed_nclauses b u)
1.42 - else prod (signed_nclauses b t) (signed_nclauses b u)
1.43 - | signed_nclauses b (Const("op |",_) $ t $ u) =
1.44 - if b then prod (signed_nclauses b t) (signed_nclauses b u)
1.45 - else sum (signed_nclauses b t) (signed_nclauses b u)
1.46 - | signed_nclauses b (Const("op -->",_) $ t $ u) =
1.47 - if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
1.48 - else sum (signed_nclauses (not b) t) (signed_nclauses b u)
1.49 - | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
1.50 - if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
1.51 - if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
1.52 - (prod (signed_nclauses (not b) u) (signed_nclauses b t))
1.53 - else sum (prod (signed_nclauses b t) (signed_nclauses b u))
1.54 - (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
1.55 - else 1
1.56 - | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
1.57 - | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
1.58 - | signed_nclauses _ _ = 1; (* literal *)
1.59 -
1.60 -val nclauses = signed_nclauses true;
1.61 -
1.62 -fun too_many_clauses t = nclauses t >= max_clauses;
1.63 +fun too_many_clauses ctxto t =
1.64 + let
1.65 + val max_cl = case ctxto of SOME ctxt => Config.get ctxt max_clauses
1.66 + | NONE => max_clauses_default
1.67 +
1.68 + fun sum x y = if x < max_cl andalso y < max_cl then x+y else max_cl;
1.69 + fun prod x y = if x < max_cl andalso y < max_cl then x*y else max_cl;
1.70 +
1.71 + (*Estimate the number of clauses in order to detect infeasible theorems*)
1.72 + fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
1.73 + | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
1.74 + | signed_nclauses b (Const("op &",_) $ t $ u) =
1.75 + if b then sum (signed_nclauses b t) (signed_nclauses b u)
1.76 + else prod (signed_nclauses b t) (signed_nclauses b u)
1.77 + | signed_nclauses b (Const("op |",_) $ t $ u) =
1.78 + if b then prod (signed_nclauses b t) (signed_nclauses b u)
1.79 + else sum (signed_nclauses b t) (signed_nclauses b u)
1.80 + | signed_nclauses b (Const("op -->",_) $ t $ u) =
1.81 + if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
1.82 + else sum (signed_nclauses (not b) t) (signed_nclauses b u)
1.83 + | signed_nclauses b (Const("op =", Type ("fun", [T, _])) $ t $ u) =
1.84 + if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
1.85 + if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
1.86 + (prod (signed_nclauses (not b) u) (signed_nclauses b t))
1.87 + else sum (prod (signed_nclauses b t) (signed_nclauses b u))
1.88 + (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
1.89 + else 1
1.90 + | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
1.91 + | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
1.92 + | signed_nclauses _ _ = 1; (* literal *)
1.93 + in
1.94 + signed_nclauses true t >= max_cl
1.95 + end;
1.96
1.97 (*Replaces universally quantified variables by FREE variables -- because
1.98 assumptions may not contain scheme variables. Later, generalize using Variable.export. *)
1.99 @@ -328,8 +334,8 @@
1.100 | _ => nodups th :: ths (*no work to do*)
1.101 and cnf_nil th = cnf_aux (th,[])
1.102 val cls =
1.103 - if too_many_clauses (concl_of th)
1.104 - then (Output.debug (fn () => ("cnf is ignoring: " ^ string_of_thm th)); ths)
1.105 + if too_many_clauses (SOME ctxt) (concl_of th)
1.106 + then (warning ("cnf is ignoring: " ^ string_of_thm th); ths)
1.107 else cnf_aux (th,ths)
1.108 in (cls, !ctxtr) end;
1.109