1.1 --- a/src/HOL/Tools/meson.ML Fri Oct 20 10:44:56 2006 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Fri Oct 20 11:03:33 2006 +0200
1.3 @@ -193,13 +193,35 @@
1.4
1.5 (*** The basic CNF transformation ***)
1.6
1.7 +val max_clauses = ref 20;
1.8 +
1.9 +fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses;
1.10 +fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses;
1.11 +
1.12 (*Estimate the number of clauses in order to detect infeasible theorems*)
1.13 -fun nclauses (Const("Trueprop",_) $ t) = nclauses t
1.14 - | nclauses (Const("op &",_) $ t $ u) = nclauses t + nclauses u
1.15 - | nclauses (Const("Ex", _) $ Abs (_,_,t)) = nclauses t
1.16 - | nclauses (Const("All",_) $ Abs (_,_,t)) = nclauses t
1.17 - | nclauses (Const("op |",_) $ t $ u) = nclauses t * nclauses u
1.18 - | nclauses _ = 1; (* literal *)
1.19 +fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
1.20 + | signed_nclauses b (Const("Not",_) $ t) = signed_nclauses (not b) t
1.21 + | signed_nclauses b (Const("op &",_) $ t $ u) =
1.22 + if b then sum (signed_nclauses b t) (signed_nclauses b u)
1.23 + else prod (signed_nclauses b t) (signed_nclauses b u)
1.24 + | signed_nclauses b (Const("op |",_) $ t $ u) =
1.25 + if b then prod (signed_nclauses b t) (signed_nclauses b u)
1.26 + else sum (signed_nclauses b t) (signed_nclauses b u)
1.27 + | signed_nclauses b (Const("op -->",_) $ t $ u) =
1.28 + if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
1.29 + else sum (signed_nclauses (not b) t) (signed_nclauses b u)
1.30 + | signed_nclauses b (Const("op =",_) $ t $ u) =
1.31 + if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
1.32 + (prod (signed_nclauses (not b) u) (signed_nclauses b t))
1.33 + else sum (prod (signed_nclauses b t) (signed_nclauses b u))
1.34 + (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
1.35 + | signed_nclauses b (Const("Ex", _) $ Abs (_,_,t)) = signed_nclauses b t
1.36 + | signed_nclauses b (Const("All",_) $ Abs (_,_,t)) = signed_nclauses b t
1.37 + | signed_nclauses _ _ = 1; (* literal *)
1.38 +
1.39 +val nclauses = signed_nclauses true;
1.40 +
1.41 +fun too_many_clauses t = nclauses t >= !max_clauses;
1.42
1.43 (*Replaces universally quantified variables by FREE variables -- because
1.44 assumptions may not contain scheme variables. Later, call "generalize". *)
1.45 @@ -247,7 +269,7 @@
1.46 | _ => (*no work to do*) th::ths
1.47 and cnf_nil th = cnf_aux (th,[])
1.48 in
1.49 - if nclauses (concl_of th) > 20
1.50 + if too_many_clauses (concl_of th)
1.51 then (Output.debug ("cnf is ignoring: " ^ string_of_thm th); ths)
1.52 else cnf_aux (th,ths)
1.53 end;