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;